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

5 files changed, 26 insertions, 26 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 8bd57b988..a4e8c056f 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -45,22 +45,22 @@ Notation "x >= y" := (NZle y x) (only parsing) : NatScope.
 
 Open Local Scope NatScope.
 
-Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A.
+Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> A.
 Implicit Arguments recursion [A].
 
 Axiom pred_0 : P 0 == 0.
 
-Axiom recursion_wd : forall (A : Set) (Aeq : relation A),
+Axiom recursion_wd : forall (A : Type) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
     forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' ->
       forall x x' : N, x == x' ->
         Aeq (recursion a f x) (recursion a' f' x').
 
 Axiom recursion_0 :
-  forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a.
+  forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a.
 
 Axiom 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 Neq Aeq Aeq f ->
       forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index d15006cb4..ad0bf445c 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -130,7 +130,7 @@ let _ =
   pr " Qed.";
   pr "";
 
-  pr " Inductive %s_ : Set :=" t;
+  pr " Inductive %s_ :=" t;
   for i = 0 to size do 
     pr "  | %s%i : w%i -> %s_" c i i t
   done;
@@ -167,7 +167,7 @@ let _ =
 
 
   pp " (* Regular make op (no karatsuba) *)";
-  pp " Fixpoint nmake_op (ww:Set) (ww_op: znz_op ww) (n: nat) : ";
+  pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : ";
   pp "       znz_op (word ww n) :=";
   pp "  match n return znz_op (word ww n) with ";
   pp "   O => ww_op";
@@ -519,7 +519,7 @@ let _ =
 
   pr " Section LevelAndIter.";
   pr "";
-  pr "  Variable res: Set.";
+  pr "  Variable res: Type.";
   pr "  Variable xxx: res.";
   pr "  Variable P: Z -> Z -> res -> Prop.";
   pr "  (* Abstraction function for each level *)";
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index ed7a7871f..c3fdd1bf4 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -120,8 +120,8 @@ Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
   reflexivity.
 Defined.
 
-Fixpoint extend (n:nat) {struct n} : forall w:Set, zn2z w -> word w (S n) :=
- match n return forall w:Set, zn2z w -> word w (S n) with 
+Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) :=
+ match n return forall w:Type, zn2z w -> word w (S n) with 
  | O => fun w x => x
  | S m => 
    let aux := extend m in
@@ -193,7 +193,7 @@ Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
       end
   end.
 
- Variable w: Set.
+ Variable w: Type.
 
  Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
      (word w (S n)) :=
@@ -219,8 +219,8 @@ Implicit Arguments castm[w m n].
 
 Section Reduce.
 
- Variable w : Set.
- Variable nT : Set.
+ Variable w : Type.
+ Variable nT : Type.
  Variable N0 : nT.
  Variable eq0 : w -> bool.
  Variable reduce_n : w -> nT.
@@ -238,8 +238,8 @@ End Reduce.
 
 Section ReduceRec.
 
- Variable w : Set.
- Variable nT : Set.
+ Variable w : Type.
+ Variable nT : Type.
  Variable N0 : nT.
  Variable reduce_1n : zn2z w -> nT.
  Variable c : forall n, word w (S n) -> nT.
@@ -269,7 +269,7 @@ Definition opp_compare cmp :=
 
 Section CompareRec.
 
- Variable wm w : Set.
+ Variable wm w : Type.
  Variable w_0 : w.
  Variable compare : w -> w -> comparison.
  Variable compare0_m : wm -> comparison.
@@ -414,7 +414,7 @@ End CompareRec.
 
 Section AddS.
 
- Variable  w wm: Set.
+ Variable w wm : Type.
  Variable incr : wm -> carry wm.
  Variable addr : w -> wm -> carry wm.
  Variable injr : w -> zn2z wm.
@@ -479,7 +479,7 @@ End AddS.
 
  Section SimplOp.
 
- Variable w: Set.
+ Variable w: Type.
 
  Theorem digits_zop: forall w (x: znz_op w),
   znz_digits (mk_zn2z_op x) = xO (znz_digits x).
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.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 506cf1df0..64f597af0 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -175,8 +175,8 @@ Qed.
 
 End NZOrdAxiomsMod.
 
-Definition recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A :=
-  fun A : Set => nat_rec (fun _ => A).
+Definition recursion : forall A : Type, A -> (nat -> A -> A) -> nat -> A :=
+  fun A : Type => nat_rect (fun _ => A).
 Implicit Arguments recursion [A].
 
 Theorem succ_neq_0 : forall n : nat, S n <> 0.
@@ -189,7 +189,7 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem recursion_wd : forall (A : Set) (Aeq : relation A),
+Theorem recursion_wd : forall (A : Type) (Aeq : relation A),
   forall a a' : A, Aeq a a' ->
     forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
       forall n n' : nat, n = n' ->
@@ -199,13 +199,13 @@ unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
 Qed.
 
 Theorem recursion_0 :
-  forall (A : Set) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
+  forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
 Proof.
 reflexivity.
 Qed.
 
 Theorem recursion_succ :
-  forall (A : Set) (Aeq : relation A) (a : A) (f : nat -> A -> A),
+  forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
     Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.