WP inserts unwanted new lines into Coq proofs
ID0002266: This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.
|ID0002266||Frama-C||Plug-in > wp||public||2017-01-02||2017-01-02|
|Product Version||Frama-C 14-Silicon||Target Version||-||Fixed in Version||-|
I have noticed (since Aluminium) that whenever I work on a Coq proof, then WP adds a newline to all the other Coq proofs in wp0.script (right before "Qed."). In the long run, it is a bit annoying to have all these empty lines in the coq proofs...