Changeset 1510 for src/common

Timestamp:

Nov 16, 2011, 4:38:41 PM (9 years ago)

Author:

sacerdot

Message:

All files ported to new dependent inversion.

Location:

src/common

Files:

• Smallstep.ma (modified) (2 diffs)
• Values.ma (modified) (1 diff)

src/common/Smallstep.ma

@@ -132 +132 @@
   plus tr ge s1 t s3.
 #tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
-[ #s2' #e2 #e3 #e4 destruct; @plus_one //;
-| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5
+[ #s2' #e2 #e3 #e4 #e5s destruct; @plus_one //;
+| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 #e6
     >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1)
     [ 2: @(star_right … H2 Hstep) //;
@@ -140 +140 @@
     ]
 ]
-qed. 
+qed.
 (*
 Lemma plus_left':

src/common/Values.ma

@@ -1098 +1098 @@
   ∀chunk,v1,v2.
   Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
-#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
-[ 8: #r ] whd in ⊢ (?%?); //; 
+#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
+[ 8: #r ] whd in ⊢ (?%?); //;
 qed.