Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2428 r2468  
    6262   learned from the hypothesis. *)
    6363#ge #ge' #en #m #RG @expr_lvalue_ind_combined
    64 [ 1,2: normalize /3 by ex_intro, conj/
     64[ 1: normalize /3 by ex_intro, conj/
    6565| * //
    6666 [ #id #ty #IH #v #tr #EX #u
     
    103103  whd in ⊢ (?(??%?)?);
    104104  cases ty' in EX1rem ⊢ %;
    105   [ 4: #ty' normalize #E destruct /2/
     105  [ 3: #ty' normalize #E destruct /2/
    106106  | *: normalize #A try #B try #C try #D destruct
    107107  ]
     
    213213| #ty #ty' #v #tr normalize /3/
    214214| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
    215   [ 7: #id #fl #IH #EX
     215  [ 6: #id #fl #IH #EX
    216216    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    217217    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
     
    221221    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    222222    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
    223   | 8: #id #fl #IH #EX
     223  | 7: #id #fl #IH #EX
    224224    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    225225    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
     
    661661        %{0} whd whd in ⊢ (??%?);
    662662        >label_function_return >E whd % /3/
    663       | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
     663      | *: #A [ 1,3,4,5,6: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    664664      ]
    665665    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
     
    699699        %{0} whd whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    700700        whd % /4/
    701       | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
     701      | *: #A [ 1,3,4,5,6: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    702702      ]
    703703    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
Note: See TracChangeset for help on using the changeset viewer.