Changeset 891 for src/Clight/CexecComplete.ma
 Timestamp:
 Jun 7, 2011, 4:53:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r879 r891 167 167  #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1) 168 168 [ #id  #e'  #e' #id ] #H3 169 whd in ⊢ (??%?); 169 whd in ⊢ (??%?) 170 [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty) 171  change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty) 172  change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty) 173 ] 170 174 >(yields_eq ??? H3) 171 whd in ⊢ (??%?); >H2 @refl 175 whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉) 176 >H2 @refl 172 177  #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); 173 178 >(yields_eq ??? H2) whd in ⊢ (??%?) … … 352 357 #ge #s #tr #s' #H elim H; 353 358 [ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?); 354 >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); 355 >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); 359 >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?) 360 >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?) 361 change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) 356 362 >H3 @refl 357 363  #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?); … … 443 449 @refl 444 450  #v #f #env #k #m @refl 445  #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?); 446 >H @refl 451  #v #f #env #k #m1 #m2 #loc #ofs #ty 452 change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v) 453 #H whd in ⊢ (??%?) >H @refl 447 454  #f #l #s #k #env #m @refl 448 455 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.