Changeset 1350 for src/common

Timestamp:

Oct 11, 2011, 2:27:53 AM (10 years ago)

Author:

sacerdot

Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

File:

• src/common/AST.ma (modified) (2 diffs)

src/common/AST.ma

@@ -354 +354 @@
     | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
       cases (map_partial … f tl) in IH ⊢ %
-      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
+      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
       >(IH x) // ]]
 qed.
@@ -486 +486 @@
  [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
  | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
-   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
+   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
    >e0 in e1; normalize #H @H ]
 qed.