Changeset 1521 for src/ASM/BitVectorTrie.ma

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:

• src/ASM/BitVectorTrie.ma (modified) (2 diffs)

src/ASM/BitVectorTrie.ma

@@ -354 +354 @@
     #t cases(BitVectorTrie_Sn … t)
     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
+     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
+     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
      [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
 qed.
@@ -458 +458 @@
     #t cases(BitVectorTrie_Sn … t)
     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
+     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
-     [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize
+     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
      [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
 qed.