switch theories/Numbers from Set to Type (both the abstract and the bignum part).

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

1 files changed, 8 insertions, 8 deletions

diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index f47cd4b38..b05acd730 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -18,20 +18,20 @@ Open Local Scope Z_scope.
 (** Iterators *)
 
 (** [n]th iteration of the function [f] *)
-Fixpoint iter_nat (n:nat) (A:Set) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
   match n with
     | O => x
     | S n' => f (iter_nat n' A f x)
   end.
 
-Fixpoint iter_pos (n:positive) (A:Set) (f:A -> A) (x:A) {struct n} : A :=
+Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
   match n with
     | xH => f x
     | xO n' => iter_pos n' A f (iter_pos n' A f x)
     | xI n' => f (iter_pos n' A f (iter_pos n' A f x))
   end.
 
-Definition iter (n:Z) (A:Set) (f:A -> A) (x:A) :=
+Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
   match n with
     | Z0 => x
     | Zpos p => iter_pos p A f x
@@ -39,7 +39,7 @@ Definition iter (n:Z) (A:Set) (f:A -> A) (x:A) :=
   end.
 
 Theorem iter_nat_plus :
-  forall (n m:nat) (A:Set) (f:A -> A) (x:A),
+  forall (n m:nat) (A:Type) (f:A -> A) (x:A),
     iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
 Proof.    
   simple induction n;
@@ -48,7 +48,7 @@ Proof.
 Qed.
 
 Theorem iter_nat_of_P :
-  forall (p:positive) (A:Set) (f:A -> A) (x:A),
+  forall (p:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos p A f x = iter_nat (nat_of_P p) A f x.
 Proof.    
   intro n; induction n as [p H| p H| ];
@@ -63,7 +63,7 @@ Proof.
 Qed.
 
 Theorem iter_pos_plus :
-  forall (p q:positive) (A:Set) (f:A -> A) (x:A),
+  forall (p q:positive) (A:Type) (f:A -> A) (x:A),
     iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x).
 Proof.    
   intros n m; intros.
@@ -78,7 +78,7 @@ Qed.
     then the iterates of [f] also preserve it. *)
 
 Theorem iter_nat_invariant :
-  forall (n:nat) (A:Set) (f:A -> A) (Inv:A -> Prop),
+  forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
     forall x:A, Inv x -> Inv (iter_nat n A f x).
 Proof.    
@@ -89,7 +89,7 @@ Proof.
 Qed.
 
 Theorem iter_pos_invariant :
-  forall (p:positive) (A:Set) (f:A -> A) (Inv:A -> Prop),
+  forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
     (forall x:A, Inv x -> Inv (f x)) ->
     forall x:A, Inv x -> Inv (iter_pos p A f x).
 Proof.