Changeset 1339 for src/common

Timestamp:

Oct 10, 2011, 4:10:32 PM (8 years ago)

Author:

sacerdot

Message:

Automation is now stronger.

File:

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

src/common/Values.ma

@@ -1186 +1186 @@
 lemma zero_ext_lessdef:
   ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
-#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
+#n #v1 #v2 #H inversion H //
 qed.
 
 lemma sign_ext_lessdef:
   ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
-#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
+#n #v1 #v2 #H inversion H //
 qed.
 (*