Make identifiers in Coq proofs more similar to those from C code
ID0001630: This issue was created automatically from Mantis Issue 1630. Further discussion may take place here.
|ID0001630||Frama-C||Plug-in > wp||public||2014-01-23||2015-03-17|
|Product Version||Frama-C Fluorine-20130601||Target Version||-||Fixed in Version||Frama-C Sodium|
When I want to proof an obligation for function foo(int* a, int n) then the Coq representation of the obligation uses the identifiers "a_0" and "n_0". In my opinion, the proofs would be easier to read if WP would generate the names "a" and "n". (I often use "remember a_0 as a" to achieve this, but it would be nicer if I did not have to do it manually.)