Changeset 1368 for src/common

Timestamp:

Oct 13, 2011, 6:11:26 PM (10 years ago)

Author:

sacerdot

Message:

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

File:

• src/common/AST.ma (modified) (1 diff)

src/common/AST.ma

@@ -201 +201 @@
 * #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct]
 cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)]
-%2 @nmk #abs -H H'; try (-H2 H2') destruct (abs) (*Wilmer: still slow destructs, why?*)
+%2 @nmk #abs -H H'; destruct (abs) (*Wilmer: still slow destructs, why?*)
 qed.