Changeset 1521 for src/Clight
 Timestamp:
 Nov 21, 2011, 1:06:01 PM (10 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r1516 r1521 88 88 >e2 89 89 whd in ⊢ (??%?); 90 change in e1:(??%?); with (make_global (mk_program ?? globs fns main))90 change with (make_global (mk_program ?? globs fns main)) in e1:(??%?); 91 91 >e1 92 92 >e3 … … 170 170 [ #id  #e'  #e' #id ] #H3 171 171 whd in ⊢ (??%?); 172 [ change in H3:(??%?); with (exec_lvalue' ge env m (Evar id) ty)173  change in H3:(??%?); with (exec_lvalue' ge env m (Ederef e') ty)174  change in H3:(??%?); with (exec_lvalue' ge env m (Efield e' id) ty)172 [ change with (exec_lvalue' ge env m (Evar id) ty) in H3:(??%?); 173  change with (exec_lvalue' ge env m (Ederef e') ty) in H3:(??%?); 174  change with (exec_lvalue' ge env m (Efield e' id) ty) in H3:(??%?); 175 175 ] 176 176 >(yields_eq ??? H3) 177 whd in ⊢ (??%?); change in H2:(??%?); with (load_value_of_type' ty m 〈l,off〉)177 whd in ⊢ (??%?); change with (load_value_of_type' ty m 〈l,off〉) in H2:(??%?); 178 178 >H2 @refl 179 179  #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); … … 362 362 >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); 363 363 >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); 364 change in H3:(??%?); with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)364 change with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) in H3:(??%?); 365 365 >H3 @refl 366 366  #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?); … … 453 453  #v #f #env #k #m @refl 454 454  #v #f #env #k #m1 #m2 #loc #ofs #ty 455 change in ⊢ (??%? → ?); with (store_value_of_type' ty m1 〈loc,ofs〉 v)455 change with (store_value_of_type' ty m1 〈loc,ofs〉 v) in ⊢ (??%? → ?); 456 456 #H whd in ⊢ (??%?); >H @refl 457 457  #f #l #s #k #env #m @refl 
src/Clight/CexecEquiv.ma
r1516 r1521 178 178  #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 179 179 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); 180 change in match (is_final ?????); with (is_final s2)180 change with (is_final s2) in match (is_final ?????); 181 181 @IFE 182 182 [ #r' #FINAL #E whd in E:(??%??); … … 420 420  #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 421 421 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); 422 change in match (is_final ?????); with (is_final s2)422 change with (is_final s2) in match (is_final ?????); 423 423 @IFE [ #r ] #F #EXECK 424 424 whd in EXECK:(??%??); destruct; … … 643 643 @(show_divergence s') 644 644 [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) 645 change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one645 change with (Eapp E0 tr1) in ⊢ (?%????); @isteps_one 646 646 @S 647 647  #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2) 648 change in ⊢ (?%????); with (Eapp E0 tr2);648 change with (Eapp E0 tr2) in ⊢ (?%????); 649 649 @isteps_one @S 650 650  #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) 651 change in ⊢ (?%????); with (Eapp E0 tr2);651 change with (Eapp E0 tr2) in ⊢ (?%????); 652 652 @(isteps_one … S) 653 653 ] … … 691 691 >E2 in H1; #H1 whd in H1:(?%?); >K' in H1; 692 692 >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); 693 change in match (is_final ?????); with (is_final s'')693 change with (is_final s'') in match (is_final ?????); 694 694 @is_final_elim 695 695 [ #r #F whd in ⊢ (?%? → ?); #S
Note: See TracChangeset
for help on using the changeset viewer.