2021-01-17 23:42 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001687Frama-CPlug-in > wppublic2014-03-12 17:00
Assigned Tocorrenson 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001687: Frama-C GUI discards candidate coq proof
DescriptionThe problem is as follows:
In a Coq proof we add the line

    repeat (rewrite shift_zero in *).

When quitting the Coq IDE, coq complains (correctly) about the token "*)" and restores the original proof,
thus completely discarding the proof attempt.
The proof attempt should at least be saved, somehow.
Additional InformationRunning release candidate of Frama-C Neon.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2014-03-12 17:00 jens New Issue
2014-03-12 17:00 jens Status new => assigned
2014-03-12 17:00 jens Assigned To => correnson
+Issue History