Changeset 1510 for src/Clight/CexecComplete.ma
 Timestamp:
 Nov 16, 2011, 4:38:41 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r1244 r1510 63 63 initial_state p s → initial_state p s' → s = s'. 64 64 #p #s #s' #H1 #H2 65 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 66 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 65 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16 66 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26 67 67 >e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14 68 68 [ 2: destruct (e1) skip (e11); @refl ] … … 84 84 #p #s cases p; #globs #fns #main #H 85 85 inversion H; 86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 #e6 87 87 whd in ⊢ (??%?); 88 88 >e2 … … 446 446 // 447 447  #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?); 448 inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 <e1 in H1 H2448 inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2 449 449 #H1 #H2 450 450 >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?); 451 whd; inversion H2; [ #sz #sg #x  #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);451 whd; inversion H2; [ #sz #sg #x  #x #sz ] #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?); 452 452 @refl 453 453  #v #f #env #k #m @refl
Note: See TracChangeset
for help on using the changeset viewer.