Changeset 2050


Ignore:
Timestamp:
Jun 12, 2012, 4:01:39 PM (5 years ago)
Author:
campbell
Message:

Limit some normalization that doesn't seem to like.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2019 r2050  
    211211    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    212212    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    213     normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
     213    whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
    214214  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    215215    %{(tr1'⧺E0⧺Echarge l5)}
    216216    whd in ⊢ (?(??%?)?); >EX1'
    217217    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    218     normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
     218    whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
    219219  ]
    220220| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
     
    230230    whd in ⊢ (?(??%?)?); >EX1'
    231231    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    232     normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
     232    whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
    233233  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    234234    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
     
    241241    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    242242    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    243     normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
     243    whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
    244244  ]
    245245| #ty #ty' #v #tr normalize /3/
Note: See TracChangeset for help on using the changeset viewer.