Changeset 1521


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.

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r1516 r1521  
    184184    #hd' * #tl' #jmeq >jmeq in h;
    185185    #new_h
    186     change in new_h; with ((andb ? ?) = ?);
     186    change with ((andb ? ?) = ?) in new_h;
    187187    cases(conjunction_true … new_h)
    188188    #eq_heads #eq_tails
     
    190190    cases(eq_b_eq … eq_heads)
    191191    whd in eq_tails:(??(?????(%))?);
    192     change in eq_tails; with (eq_bv ??? = ?);
     192    change with (eq_bv ??? = ?) in eq_tails;
    193193    <(ih tl') //
    194194  ]
  • src/ASM/BitVectorTrie.ma

    r1516 r1521  
    354354    #t cases(BitVectorTrie_Sn … t)
    355355    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    356      [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     356     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
    357357    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    358      [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     358     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
    359359     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    360360qed.
     
    458458    #t cases(BitVectorTrie_Sn … t)
    459459    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    460      [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     460     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
    461461    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    462      [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     462     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
    463463     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
    464464qed.
  • src/ASM/Status.ma

    r1518 r1521  
    940940      @ H1
    941941      cut (n ≤ S y → n - S m ≤ y)
    942       /2/
     942      /2 by/
    943943      cases n
    944944      normalize
  • 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
  • src/Cminor/toRTLabs.ma

    r1516 r1521  
    2828      whd in E:(??%?); destruct;
    2929      whd >lookup_add_hit % #A destruct
    30     | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)
     30    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
    3131      lapply (refl ? (populate_env e u tl))
    3232      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
     
    4444[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
    4545| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
    46   change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)
     46  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
    4747  lapply (refl ? (populate_env e u tl))
    4848  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
     
    6565[ #lbls #u #lbls' #u' #E #l *
    6666| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
    67   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
     67  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
    6868  lapply (refl ? (populate_label_env lbls u t))
    6969  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     
    8282[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
    8383| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
    84   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
     84  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
    8585  lapply (refl ? (populate_label_env lbls u t))
    8686  cases (populate_label_env lbls u t) in ⊢ (???% → %);
  • src/RTLabs/RTLabsToRTL.ma

    r1515 r1521  
    3232   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
    3333 #globals #def #left #right
    34  whd in match complete_regs normalize nodelta
     34 whd in match complete_regs; normalize nodelta
    3535 @leb_elim normalize nodelta #H
    36  [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
    37  | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
     36 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)));
     37 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));]
    3838 cases (fresh_regs ????) #def' #fresh normalize >append_length
    39  generalize in match H -H;
    40  generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
    41  [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
     39 generalize in match H; -H;
     40 generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh);
     41 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H); -H #H #E >E >commutative_plus
    4242         <plus_minus_m_m /2/ ]
    4343qed.
  • src/joint/TranslateUtils.ma

    r1516 r1521  
    2323  | #m whd in ⊢ (? → ??(??%)?); whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) ;
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    25     #def' #regs #EQ change in EQ; with (|regs| = m) <EQ
     25    #def' #regs #EQ change with (|regs| = m)in EQ; <EQ
    2626    @refl
    2727 ]
  • src/utilities/binary/Z.ma

    r1517 r1521  
    522522[ //;
    523523| #m' >Zpred_pos_succ
    524     change in ⊢ (??(??%)?); with (Zsucc (pos m'))
     524    change with (Zsucc (pos m')) in ⊢ (??(??%)?);
    525525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
    526526| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
Note: See TracChangeset for help on using the changeset viewer.