Ignore:
Timestamp:
Nov 16, 2011, 4:38:41 PM (9 years ago)
Author:
sacerdot
Message:

All files ported to new dependent inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1410 r1510  
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    281281[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    282 | #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
     282| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind
    283283    @(eval_lvalue_inv_ind … H1)
    284284    [ #a #b #c #d #bad destruct (bad);
     
    288288    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    289289    ]
    290 | #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); @H'
     290| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    291291| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    292292| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
Note: See TracChangeset for help on using the changeset viewer.