Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001687Frama-CPlug-in > wppublic2014-03-12 17:002014-03-12 17:00
Assigned Tocorrenson 
PlatformOSOS Version
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

- Relationships

-  Notes
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker