Changeset 1401 for src/common


Ignore:
Timestamp:
Oct 18, 2011, 12:39:11 PM (8 years ago)
Author:
ricciott
Message:

Changes concerning the new behavior of destruct.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1368 r1401  
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    201 * #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct]
    202 cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)]
    203 %2 @nmk #abs -H H'; destruct (abs) (*Wilmer: still slow destructs, why?*)
     201* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
    204202qed.
    205203
Note: See TracChangeset for help on using the changeset viewer.