Changeset 891 for src/common/Values.ma

Timestamp:

Jun 7, 2011, 4:53:53 PM (9 years ago)

Author:

campbell

Message:

Revise proofs affected by recent matita change.

File:

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

src/common/Values.ma

@@ -64 +64 @@
 | @H2 % #E destruct elim H3 /2/
 ] qed.
+
+lemma eq_block_b_b : ∀b. eq_block b b = true.
+* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
+qed.
 
 (* Characterise the memory regions which the pointer representations can
@@ -1225 +1229 @@
 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 <e1 in H >e2 //;
+#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
 qed.
 (*