Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r879 r891  
    167167| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    168168    [ #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    ]
    170174    >(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
    172177| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
    173178    >(yields_eq ??? H2) whd in ⊢ (??%?)
     
    352357#ge #s #tr #s' #H elim H;
    353358[ #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)
    356362    >H3 @refl
    357363| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     
    443449    @refl
    444450| #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
    447454| #f #l #s #k #env #m @refl
    448455] qed.
Note: See TracChangeset for help on using the changeset viewer.