Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 9 insertions, 16 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 4ef91362f..5284afe95 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -9,7 +9,7 @@
 
 Require Export BinNums.
 Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
- Equalities Orders GenericMinMax Le Plus Wf_nat.
+ Equalities Orders GenericMinMax Le Plus.
 
 Require Export BinPosDef.
 
@@ -38,10 +38,6 @@ Module Pos
 
 Include BinPosDef.Pos.
 
-(* TODO : fix the location of iter_nat *)
-Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
-Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p.
-
 (** * Logical Predicates *)
 
 Definition eq := @Logic.eq t.
@@ -1882,7 +1878,7 @@ Notation Pminus_mask := Pos.sub_mask (only parsing).
 Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
 Notation Pminus := Pos.sub (only parsing).
 Notation Pmult := Pos.mul (only parsing).
-Notation iter_pos p A := (@Pos.iter p A) (only parsing).
+Notation iter_pos := @Pos.iter (only parsing).
 Notation Ppow := Pos.pow (only parsing).
 Notation Pdiv2 := Pos.div2 (only parsing).
 Notation Pdiv2_up := Pos.div2_up (only parsing).
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index cf7e450f4..9b6081176 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -478,11 +478,8 @@ Fixpoint lxor (p q:positive) : N :=
 
 (** Shifts. NB: right shift of 1 stays at 1. *)
 
-(*
-Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
-
-Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p.
-*)
+Definition shiftl_nat (p:positive)(n:nat) := nat_iter n xO p.
+Definition shiftr_nat (p:positive)(n:nat) := nat_iter n div2 p.
 
 Definition shiftl (p:positive)(n:N) :=
   match n with
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 5c46c8210..a0ca9f5b6 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec Wf_nat.
+Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec.
 
 (** Properties of the injection from binary positive numbers
     to Peano natural numbers *)
@@ -143,11 +143,11 @@ Proof.
  now apply lt_le_weak, inj_lt.
 Qed.
 
-(** [Pos.to_nat] is a morphism for [iter_pos] and [iter_nat] *)
+(** [Pos.to_nat] is a morphism for [Pos.iter] and [nat_iter] *)
 
 Theorem inj_iter :
-  forall p (A:Type) (f:A->A) (x:A),
-    Pos.iter p f x = iter_nat (to_nat p) _ f x.
+  forall p {A} (f:A->A) (x:A),
+    Pos.iter p f x = nat_iter (to_nat p) f x.
 Proof.
  induction p using peano_ind. trivial.
  intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
@@ -298,7 +298,7 @@ Notation Pgt_gt := Pos2Nat.inj_gt (only parsing).
 Notation Ple_le := Pos2Nat.inj_le (only parsing).
 Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
 Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
-Notation iter_nat_of_P := Pos2Nat.inj_iter (only parsing).
+Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).
 
 Notation nat_of_P_of_succ_nat := SuccNat2Pos.bij (only parsing).
 Notation P_of_succ_nat_of_P := Pos2SuccNat.bij (only parsing).