Changeset 2184

Timestamp:

Jul 13, 2012, 7:59:41 PM (6 years ago)

Author:

campbell

Message:

Minor fix ups.

Location:

src

Files:

• Clight/SimplifyCasts.ma (modified) (1 diff)
• RTLabs/Traces.ma (modified) (4 diffs)

src/Clight/SimplifyCasts.ma

@@ -3036 +3036 @@
      whd in match (exec_step ??) in ⊢ (% → %);
      #Habsurd destruct (Habsurd)
-] 
+] qed. 

src/RTLabs/Traces.ma

@@ -799 +799 @@
   >Estmt #LP whd in ⊢ (??%? → ?);
   (* replace with lemma on successors? *)
-  @bind_res_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
+  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
   [ 2: (* later *)
   | *: #E destruct
@@ -836 +836 @@
 cases fd
 [ #fn whd in ⊢ (??%? → % → ?);
-  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
+  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
   #m' #b whd in ⊢ (??%? → ?); #E' destruct
   * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
@@ -1497 +1497 @@
 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
-  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] 
+  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ] 
   whd in ⊢ (??%? → ?);
   generalize in ⊢ (??(?%)? → ?);
@@ -1589 +1589 @@
 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
-  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] 
+  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ] 
   whd in ⊢ (??%? → ?);
   generalize in ⊢ (??(?%)? → ?);