Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001626Frama-CPlug-in > wppublic2014-01-22 14:192014-03-13 15:57
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001626: Qedlib.v definition of tactic "replace by" clashes with standard tactic "replace with"
DescriptionI cannot use the standard coq tactic "replace with" because it clashes (apparently with
"replace by" defined in Qedlib.v)
Steps To ReproduceJust try to use "replace A by B" in a coq proof of a wp proof obligation
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004495)
correnson (manager)
2014-02-05 13:44

The workaround is to used the Qed definition instead, which is more powerful since it simplifies the resulting side proof obligations.
However, we shall use another name instead.
(0004496)
correnson (manager)
2014-02-05 13:44

Feature wish
(0004525)
correnson (manager)
2014-02-07 10:23

Fix committed to feature/wp_migration_why3 branch.
(0004526)
correnson (manager)
2014-02-07 14:03

Fix committed to feature/wp_migration_why3 branch.
(0004527)
correnson (manager)
2014-02-07 14:39

Fix committed to feature/wp_migration_why3 branch.
(0004528)
correnson (manager)
2014-02-07 15:46

Fix committed to master branch.
(0004532)
correnson (manager)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2014-01-22 14:19 jens New Issue
2014-01-22 14:19 jens Status new => assigned
2014-01-22 14:19 jens Assigned To => correnson
2014-02-05 13:44 correnson Note Added: 0004495
2014-02-05 13:44 correnson Note Added: 0004496
2014-02-05 13:44 correnson Status assigned => acknowledged
2014-02-07 10:23 correnson Note Added: 0004525
2014-02-07 10:23 correnson Status acknowledged => resolved
2014-02-07 10:23 correnson Resolution open => fixed
2014-02-07 14:03 correnson Note Added: 0004526
2014-02-07 14:39 correnson Note Added: 0004527
2014-02-07 15:46 correnson Note Added: 0004528
2014-02-12 16:57 correnson Note Added: 0004532
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker