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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.