diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-25 16:17:15 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-05-02 11:05:19 +0200 |
| commit | 1432318faa4cb6a50eca2c7a371b43b3b9969666 (patch) | |
| tree | 694d6a8266ec1aad5f0439cfb0a3fa41fb8fd270 /theories/ZArith/BinInt.v | |
| parent | c3e091756e0030e29e231ca1d7c3bd12ded55760 (diff) | |
Pos.iter arguments in a better order for cbn.
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 6948d420a..452e3d148 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -959,7 +959,7 @@ Proof. destruct m; easy || now destruct Hm. destruct a as [ |a|a]. (* a = 0 *) - replace (Pos.iter n div2 0) with 0 + replace (Pos.iter div2 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. (* a > 0 *) @@ -982,7 +982,7 @@ Proof. rewrite ?Pos.iter_succ; apply testbit_even_0. destruct a as [ |a|a]. (* a = 0 *) - replace (Pos.iter n (mul 2) 0) with 0 + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). apply testbit_0_l. (* a > 0 *) @@ -1013,7 +1013,7 @@ Proof. f_equal. now rewrite Pos.add_comm, Pos.add_sub. destruct a; unfold shiftl. (* ... a = 0 *) - replace (Pos.iter n (mul 2) 0) with 0 + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. (* ... a > 0 *) |