Pos.iter arguments in a better order for cbn.

2 files changed, 4 insertions, 4 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 61a77bf0e..256dce782 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -944,7 +944,7 @@ Proof.
  destruct n as [|n]; simpl in *.
  destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
  rewrite Pos.iter_succ. simpl.
- set (u:=Pos.iter n xO p) in *; clearbody u.
+ set (u:=Pos.iter xO p n) in *; clearbody u.
  destruct m as [|m]. now destruct u.
  rewrite <- (IHn (Pos.pred_N m)).
  rewrite <- (testbit_odd_succ _ (Pos.pred_N m)).
@@ -968,7 +968,7 @@ Proof.
  rewrite <- IHn.
  rewrite testbit_succ_r_div2 by apply le_0_l.
  f_equal. simpl. rewrite Pos.iter_succ.
- now destruct (Pos.iter n xO p).
+ now destruct (Pos.iter xO p n).
  apply succ_le_mono. now rewrite succ_pos_pred.
 Qed.
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index c4e6bd254..6aeeccaf5 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -337,7 +337,7 @@ Definition shiftl a n :=
 Definition shiftr a n :=
   match n with
     | 0 => a
-    | pos p => Pos.iter p div2 a
+    | pos p => Pos.iter div2 a p
   end.
 
 (** Checking whether a particular bit is set or not *)
@@ -375,7 +375,7 @@ Definition of_nat (n:nat) :=
 Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
   match n with
     | 0 => x
-    | pos p => Pos.iter p f x
+    | pos p => Pos.iter f x p
   end.
 
 End N.
\ No newline at end of file