Changeset 2050 for src

Timestamp:

Jun 12, 2012, 4:01:39 PM (9 years ago)

Author:

campbell

Message:

Limit some normalization that doesn't seem to like.

File:

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

src/Clight/labelSimulation.ma

@@ -211 +211 @@
     whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
     whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
-    normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
+    whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
   | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
     %{(tr1'⧺E0⧺Echarge l5)}
     whd in ⊢ (?(??%?)?); >EX1'
     whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
-    normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
+    whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
   ]
 | #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
@@ -230 +230 @@
     whd in ⊢ (?(??%?)?); >EX1'
     whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
-    normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
+    whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
   | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
     cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
@@ -241 +241 @@
     whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
     whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
-    normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
+    whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
   ]
 | #ty #ty' #v #tr normalize /3/