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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r2176 r2353 383 383 >(yields_eq ??? (bool_of_false ?? H2)) 384 384 @refl 385  #f #e #s # k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);386 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); 387 >(yields_eq ??? (bool_of_false ?? H2)) 388 @refl 389  #f #e #s # k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?);390 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); 391 >(yields_eq ??? (bool_of_true ?? H2)) 392 @refl 393  #f #s1 #e #s2 # k #env #m #H cases H; #es1 >es1 @refl394  13,14: #f #e #s #k #env #m @refl385  #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); 386 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); 387 >(yields_eq ??? (bool_of_false ?? H2)) 388 @refl 389  #f #e #s #cl #k #env #m #v #tr #H1 #H2 whd in ⊢ (??%?); 390 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); 391 >(yields_eq ??? (bool_of_true ?? H2)) 392 @refl 393  #f #s1 #e #s2 #cl #k #env #m #H cases H; #es1 >es1 @refl 394  13,14: #f #e #s [#cl] #k #env #m @refl 395 395  #f #s1 #e #s2 #k #env #m #v #tr *; #es1 >es1 #H1 #H2 whd in ⊢ (??%?); 396 396 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); … … 424 424 [ #H1 #H2 whd in ⊢ (??%?); >H2 @refl 425 425  #s' #k' whd in ⊢ (% → ?); *; 426  3,4: #e' #s' #k' whd in ⊢ (% → ?); *;426  3,4: #e' #s' [#cl] #k' whd in ⊢ (% → ?); *; 427 427  5,6: #e' #s1' #s2' #k' whd in ⊢ (% → ?); *; 428 428  #k' whd in ⊢ (% → ?); *;
Note: See TracChangeset
for help on using the changeset viewer.