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, 4 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index c2af66724..170dfa42f 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -197,7 +197,7 @@ Qed.
 
 End NZOrdAxiomsMod.
 
-Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) :=
+Definition recursion (A : Type) (a : A) (f : N -> A -> A) (n : N) :=
   Nrect (fun _ => A) a f n.
 Implicit Arguments recursion [A].
 
@@ -207,7 +207,7 @@ reflexivity.
 Qed.
 
 Theorem recursion_wd :
-forall (A : Set) (Aeq : relation A),
+forall (A : Type) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
     forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
       forall x x' : N, x = x' ->
@@ -224,13 +224,13 @@ now apply Eff'; [| apply IH].
 Qed.
 
 Theorem recursion_0 :
-  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f N0 = a.
+  forall (A : Type) (a : A) (f : N -> A -> A), recursion a f N0 = a.
 Proof.
 intros A a f; unfold recursion; now rewrite Nrect_base.
 Qed.
 
 Theorem recursion_succ :
-  forall (A : Set) (Aeq : relation A) (a : A) (f : N -> A -> A),
+  forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
     Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
       forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.