Changeset 1566 for src/Clight/CexecComplete.ma
- Timestamp:
- Nov 25, 2011, 6:12:47 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecComplete.ma
r1545 r1566 123 123 P e. 124 124 #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; // 130 130 ] qed. 131 131
Note: See TracChangeset
for help on using the changeset viewer.