Changeset 1521 for src/Clight


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

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

Location:
src/Clight
Files:
2 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
  • src/Clight/CexecEquiv.ma

    r1516 r1521  
    178178            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    179179                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 ?????);
    181181                @IFE
    182182                [ #r' #FINAL #E whd in E:(??%??);
     
    420420            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    421421                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 ?????);
    423423                @IFE [ #r ] #F #EXECK
    424424                whd in EXECK:(??%??); destruct;
     
    643643      @(show_divergence s')
    644644      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
    645         change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one
     645        change with (Eapp E0 tr1) in ⊢ (?%????); @isteps_one
    646646        @S
    647647      | #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 ⊢ (?%????);
    649649          @isteps_one @S
    650650      | #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 ⊢ (?%????);
    652652          @(isteps_one … S)
    653653      ]
     
    691691    >E2 in H1; #H1 whd in H1:(?%?); >K' in H1;
    692692    >(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 ?????);
    694694    @is_final_elim
    695695    [ #r #F whd in ⊢ (?%? → ?); #S
Note: See TracChangeset for help on using the changeset viewer.