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
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker