Pos.iter arguments in a better order for cbn.

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 4541fce0d..aed4fef05 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -195,16 +195,16 @@ Infix "*" := mul : positive_scope.
 
 (** ** Iteration over a positive number *)
 
-Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A :=
-  match n with
+Definition iter {A} (f:A -> A) : A -> positive -> A :=
+  fix iter_fix x n := match n with
     | xH => f x
-    | xO n' => iter n' f (iter n' f x)
-    | xI n' => f (iter n' f (iter n' f x))
+    | xO n' => iter_fix (iter_fix x n') n'
+    | xI n' => f (iter_fix (iter_fix x n') n')
   end.
 
 (** ** Power *)
 
-Definition pow (x y:positive) := iter y (mul x) 1.
+Definition pow (x:positive) := iter (mul x) 1.
 
 Infix "^" := pow : positive_scope.
 
@@ -488,13 +488,13 @@ Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2).
 Definition shiftl (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n xO p
+    | Npos n => iter xO p n
   end.
 
 Definition shiftr (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n div2 p
+    | Npos n => iter div2 p n
   end.
 
 (** Checking whether a particular bit is set or not *)