Ignore:
Timestamp:
Nov 21, 2011, 1:06:01 PM (8 years ago)
Author:
sacerdot
Message:

Syntax change in Matita: change what where => change where what.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1516 r1521  
    8888>e2
    8989whd in ⊢ (??%?);
    90 change in e1:(??%?); with (make_global (mk_program ?? globs fns main))
     90change with (make_global (mk_program ?? globs fns main)) in e1:(??%?);
    9191>e1
    9292>e3
     
    170170    [ #id | #e' | #e' #id ] #H3
    171171    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:(??%?);
    175175    ]
    176176    >(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:(??%?);
    178178    >H2 @refl
    179179| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
     
    362362    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
    363363    >(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:(??%?);
    365365    >H3 @refl
    366366| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     
    453453| #v #f #env #k #m @refl
    454454| #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 ⊢ (??%? → ?);
    456456    #H whd in ⊢ (??%?); >H @refl
    457457| #f #l #s #k #env #m @refl
Note: See TracChangeset for help on using the changeset viewer.