Changeset 1368


Ignore:
Timestamp:
Oct 13, 2011, 6:11:26 PM (8 years ago)
Author:
sacerdot
Message:

A bug in the clear tactic makes the previous (correct) commit wrong.
Fixed by omitting the clear.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1367 r1368  
    201201* #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct]
    202202cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)]
    203 %2 @nmk #abs -H H'; try (-H2 H2') destruct (abs) (*Wilmer: still slow destructs, why?*)
     203%2 @nmk #abs -H H'; destruct (abs) (*Wilmer: still slow destructs, why?*)
    204204qed.
    205205
Note: See TracChangeset for help on using the changeset viewer.