Allow starting coq from Frama-C GUI also for proven obligations
ID0001623: This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.
|ID0001623||Frama-C||Plug-in > wp||public||2014-01-21||2014-03-13|
|Platform||-||OS||Linux, OSX||OS Version||-|
|Product Version||Frama-C Fluorine-20130601||Target Version||-||Fixed in Version||Frama-C Neon-20140301|
Currently it is not possible to start the codide from the Frama-C GUI for a proof obligation that has already been proven by Coq. However, it would be desirable to do so in order to improve/refactor an already existing proof.