Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (8 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1521 r1545  
    104104| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
     106| #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc'
    107107    elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
    108108    whd in ⊢ (??%?);
     
    134134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    135135    >(eq_bv_false … ne) //
    136   | #r #b #pc #i #i0 #s %{ true} % //
     136  | * #r #b #pc #i #i0 #s %{ true} % //
    137137  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    138138  | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //
     
    145145#v #ty #H elim H;
    146146  [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //;
    147   | #p #b #i #i0 #s //
     147  | * #p #b #i #i0 #s //
    148148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
    149149  ]
Note: See TracChangeset for help on using the changeset viewer.