Changeset 1521 for src/ASM


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/ASM
Files:
3 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
Note: See TracChangeset for help on using the changeset viewer.