Changeset 2176 for src/Clight/labelSimulation.ma

Timestamp:

Jul 12, 2012, 1:28:28 PM (7 years ago)

Author:

campbell

Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:

• src/Clight/labelSimulation.ma (modified) (3 diffs)

src/Clight/labelSimulation.ma

@@ -103 +103 @@
   whd in ⊢ (?(??%?)?); 
   cases ty' in EX1rem ⊢ %;
-  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
-       #pc normalize #E destruct /2/
+  [ 4: #ty' normalize #E destruct /2/
   | *: normalize #A try #B try #C try #D destruct
   ]
@@ -672 +671 @@
         % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
         | // ] | /3/ ]
-      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
+      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
       ]
     | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
@@ -720 +719 @@
         %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
         @refl | // ] | /4/ ] | skip ]
-      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
+      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
       ]
     | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct