Changeset 874 for src

Timestamp:

Jun 3, 2011, 10:13:35 AM (9 years ago)

Author:

sacerdot

Message:

Tactics no longer works.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -333 +333 @@
   try %
   [ 2: cases (sym_eq ??? prf); @tl
-  | cases prf in tl H; #tl
+  | generalize in match H; generalize in match tl; cases prf;
+    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
+    #tl
     normalize in ⊢ (∀_: %. ?)
     # H