Ignore:
Timestamp:
Nov 25, 2011, 6:12:47 PM (9 years ago)
Author:
campbell
Message:

Pacify changes to destruct tactic.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1545 r1566  
    123123  P e.
    124124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125 [ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126 | #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127 | #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     125[ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
     126| #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
     127| #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
     128| #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
     129| #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
    130130] qed.
    131131
Note: See TracChangeset for help on using the changeset viewer.