aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/BinNatDef.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/NArith/BinNatDef.v')
-rw-r--r--theories/NArith/BinNatDef.v4
1 files changed, 2 insertions, 2 deletions
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