Changeset 2025 for src/RTLabs/Traces.ma

Timestamp:

Jun 7, 2012, 3:51:11 PM (8 years ago)

Author:

campbell

Message:

Silly typo and old comment.

File:

• src/RTLabs/Traces.ma (modified) (12 diffs)

src/RTLabs/Traces.ma

@@ -563 +563 @@
   well_cost_labelled_state s →
   well_cost_labelled_state s'.
-#ge #s #tr' #s' #EV cases (eval_perserves … EV)
+#ge #s #tr' #s' #EV cases (eval_preserves … EV)
 [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
 | #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
@@ -772 +772 @@
   eval_statement ge s1 = Value ??? 〈tr,s2〉 →
   stack_preserved doesnt_end_with_ret s1 s2.
-#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
+#ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
 [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
 | #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
@@ -794 +794 @@
 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
 | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
-  inversion (eval_perserves … EV)
+  inversion (eval_preserves … EV)
   [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
   | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
@@ -808 +808 @@
   ]
 | #s1 #r #S1 #E1 #E2 #E3 #_ destruct
-  inversion (eval_perserves … EV)
+  inversion (eval_preserves … EV)
   [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
   | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
@@ -834 +834 @@
 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
 | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
-  inversion (eval_perserves … EV)
+  inversion (eval_preserves … EV)
   [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
   | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
@@ -848 +848 @@
   ]
 | #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
-  inversion (eval_perserves … EV)
+  inversion (eval_preserves … EV)
   [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
   | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
@@ -1446 +1446 @@
     *)
     @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
-    inversion (eval_perserves … EVAL)
+    inversion (eval_preserves … EVAL)
     [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
       >(eval_steps … EVAL) in E2; #En normalize in En;
@@ -1471 +1471 @@
   /3/
 | #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
-  #EVAL #NC %2 inversion (eval_perserves … EVAL)
+  #EVAL #NC %2 inversion (eval_preserves … EVAL)
   [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
   | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
@@ -1526 +1526 @@
   soundly_labelled_state s'.
 #ge #s #tr #s' #ENV #EV #S
-inversion (eval_perserves … EV)
+inversion (eval_preserves … EV)
 [ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct 
   whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
@@ -1632 +1632 @@
   RTLabs_is_final s' = None ?.
 #ge #s #tr #s' #EV
-inversion (eval_perserves … EV) //
+inversion (eval_preserves … EV) //
 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
 @⊥ @(absurd ?? CL) @refl
@@ -1718 +1718 @@
       | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
         cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
-        inversion (eval_perserves … EV)
+        inversion (eval_preserves … EV)
         [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
         #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
@@ -1831 +1831 @@
 @bind_ok #f #_
 #E destruct
-#EV #SP inversion (eval_perserves … EV)
+#EV #SP inversion (eval_preserves … EV)
 [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
      inversion SP