Changeset 2353 for src/Clight/CexecEquiv.ma
 Timestamp:
 Sep 26, 2012, 6:14:38 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecEquiv.ma
r1713 r2353 514 514 #ge #s cases s; 515 515 [ #f #st #kk #e #m cases st; 516 [ 11,14: #a  2,4, 6,7,12,13,15: #a #b  3,5: #a #b #c  8: #a #b #c #d ]517 [ 4, 6,8,9: @I ]516 [ 11,14: #a  2,4,7,12,13,15: #a #b  3,5,6: #a #b #c  8: #a #b #c #d ] 517 [ 4,5,7,8: @I ] 518 518 whd in ⊢ (???%); 519 519 [ cases a; [ cases (fn_return f); //;  #e whd nodelta in ⊢ (???%); … … 521 521  cases (find_label a (fn_body f) (call_cont kk)); [ @I  #z cases z #x #y @I ] 522 522  @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I 523  4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I524 523  @err2_does_not_interact #x1 #x2 cases x1; //; 525 524  @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @err_does_not_interact #x6 cases a; 526 525 [ @I  #x7 @err2_does_not_interact #x8 #x9 @I ] 526  6,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I 527 527  cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I 528 528  @I ]
Note: See TracChangeset
for help on using the changeset viewer.