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