2021-02-27 11:29 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001626Frama-CPlug-in > wppublic2014-03-13 15:57
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0004495

correnson (manager)

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)

Feature wish

~0004525

correnson (manager)

Fix committed to feature/wp_migration_why3 branch.

~0004526

correnson (manager)

Fix committed to feature/wp_migration_why3 branch.

~0004527

correnson (manager)

Fix committed to feature/wp_migration_why3 branch.

~0004528

correnson (manager)

Fix committed to master branch.

~0004532

correnson (manager)

Fix committed to stable/neon branch.
+Notes

-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 Source_changeset_attached => framac feature/wp_migration_why3 302e12c2
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 Source_changeset_attached => framac feature/wp_migration_why3 b4564c2c
2014-02-07 14:03 correnson Note Added: 0004526
2014-02-07 14:39 correnson Source_changeset_attached => framac feature/wp_migration_why3 a0d8e74d
2014-02-07 14:39 correnson Note Added: 0004527
2014-02-07 15:46 correnson Source_changeset_attached => framac master a0d8e74d
2014-02-07 15:46 correnson Note Added: 0004528
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon a0d8e74d
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
+Issue History