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

22 files changed, 87 insertions, 72 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 4bd2331e1e..ed099a1fd2 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -28,9 +28,9 @@ Open Local Scope Z_scope.
 
 Section Z_nZ_Op.
 
- Variable znz : Set.
+ Variable znz : Type.
 
- Record znz_op : Set := mk_znz_op {
+ Record znz_op := mk_znz_op {
 
     (* Conversion functions with Z *)
     znz_digits : positive;  
@@ -76,7 +76,7 @@ Section Z_nZ_Op.
     znz_square_c    : znz -> zn2z znz;
 
     (* Special divisions operations *)
-    znz_div21       : znz -> znz -> znz -> znz*znz; (* very ad-hoc ?? *)
+    znz_div21       : znz -> znz -> znz -> znz*znz;
     znz_div_gt      : znz -> znz -> znz * znz; (* why this one ? *)
     znz_div         : znz -> znz -> znz * znz;
 
@@ -85,18 +85,22 @@ Section Z_nZ_Op.
 
     znz_gcd_gt      : znz -> znz -> znz; (* why this one ? *)
     znz_gcd         : znz -> znz -> znz; 
-    znz_add_mul_div : znz -> znz -> znz -> znz; (* very ad-hoc *)
+    (* [znz_add_mul_div p i j] is a combination of the [(digits-p)]
+       low bits of [i] above the [p] high bits of [j]: 
+       [znz_add_mul_div p i j = i*2^p+j/2^(digits-p)] *)
+    znz_add_mul_div : znz -> znz -> znz -> znz;
+    (* [znz_pos_mod p i] is [i mod 2^p] *)
     znz_pos_mod     : znz -> znz -> znz;
 
-   (* square root *)
     znz_is_even     : znz -> bool;
+    (* square root *)
     znz_sqrt2       : znz -> znz -> znz * carry znz;
     znz_sqrt        : znz -> znz  }.
 
 End Z_nZ_Op.
 
 Section Z_nZ_Spec.
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
 
  Let w_digits      := w_op.(znz_digits).
@@ -170,7 +174,7 @@ Section Z_nZ_Spec.
  Notation "[|| x ||]" :=
    (zn2z_to_Z wB w_to_Z x)  (at level 0, x at level 99).
 
- Record znz_spec : Set := mk_znz_spec {
+ Record znz_spec := mk_znz_spec {
 
     (* Conversion functions with Z *)
     spec_to_Z   : forall x, 0 <= [| x |] < wB;
@@ -281,13 +285,13 @@ End Z_nZ_Spec.
 
 Section znz_of_pos.
  
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
  Variable op_spec : znz_spec w_op.
 
  Notation "[| x |]" := (znz_to_Z w_op x)  (at level 0, x at level 99).
 
- Definition znz_of_Z (w:Set) (op:znz_op w) z :=
+ Definition znz_of_Z (w:Type) (op:znz_op w) z :=
  match z with
  | Zpos p => snd (op.(znz_of_pos) p)
  | _ => op.(znz_0)
@@ -325,7 +329,7 @@ End znz_of_pos.
 (** A modular specification grouping the earlier records. *)
 
 Module Type CyclicType.
- Parameter w : Set.
+ Parameter w : Type.
  Parameter w_op : znz_op w.
  Parameter w_spec : znz_spec w_op.
 End CyclicType.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index d198361f15..d60af33ecb 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleAdd.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_1 : w.
  Variable w_WW : w -> w -> zn2z w.
@@ -76,7 +76,7 @@ Section DoubleAdd.
     end
   end.
 
- Variable R : Set.
+ Variable R : Type.
  Variable f0 f1 : zn2z w -> R.
 
  Definition ww_add_c_cont x y :=
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 3d1d1c235a..37b9f47b49 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -19,7 +19,7 @@ Require Import DoubleType.
 Open Local Scope Z_scope.
 
 Section DoubleBase.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0   : w.
  Variable w_1   : w.
  Variable w_Bm1 : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 54ff3d3545..0a8b281fb1 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -30,7 +30,7 @@ Open Local Scope Z_scope.
 
 Section Z_2nZ.
 
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
  Let w_digits      := w_op.(znz_digits).
  Let w_zdigits      := w_op.(znz_zdigits).
@@ -890,7 +890,7 @@ End Z_2nZ.
  
 Section MulAdd.
  
-  Variable w: Set.
+  Variable w: Type.
   Variable op: znz_op w.
   Variable sop: znz_spec op.
 
@@ -918,5 +918,16 @@ Section MulAdd.
 End MulAdd.
 
 
+(** Modular versions of DoubleCyclic *) 
 
- 
+Module DoubleCyclic (C:CyclicType) <: CyclicType.
+ Definition w := zn2z C.w.
+ Definition w_op := mk_zn2z_op C.w_op.
+ Definition w_spec := mk_znz2_spec C.w_spec.
+End DoubleCyclic.
+
+Module DoubleCyclicKaratsuba (C:CyclicType) <: CyclicType.
+ Definition w := zn2z C.w.
+ Definition w_op := mk_zn2z_op_karatsuba C.w_op.
+ Definition w_spec := mk_znz2_karatsuba_spec C.w_spec.
+End DoubleCyclicKaratsuba.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index cac2cc5b57..d3dfd2505c 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -27,7 +27,7 @@ Ltac zarith := auto with zarith.
 
 Section POS_MOD.
 
- Variable w:Set.
+ Variable w:Type.
  Variable w_0 : w.
  Variable w_digits : positive.
  Variable w_zdigits : w.
@@ -201,7 +201,7 @@ End POS_MOD.
 
 Section DoubleDiv32.
 
- Variable w             : Set.
+ Variable w             : Type.
  Variable w_0           : w.
  Variable w_Bm1         : w.
  Variable w_Bm2         : w.
@@ -473,7 +473,7 @@ Section DoubleDiv32.
 End DoubleDiv32.
 
 Section DoubleDiv21.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
 
  Variable w_0W : w -> zn2z w.
@@ -634,7 +634,7 @@ Section DoubleDiv21.
 End DoubleDiv21.
 
 Section DoubleDivGt.
- Variable w : Set.
+ Variable w : Type.
  Variable w_digits : positive.
  Variable w_0 : w.
 
@@ -1344,7 +1344,7 @@ End DoubleDivGt.
 
 Section DoubleDiv.
 
- Variable w : Set.
+ Variable w : Type.
  Variable w_digits : positive.
  Variable ww_1 : zn2z w.
  Variable ww_compare : zn2z w -> zn2z w -> comparison.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 00ba4e4eed..1f1d609f1d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -21,7 +21,7 @@ Open Local Scope Z_scope.
 
 Section GENDIVN1.
 
- Variable w             : Set.
+ Variable w             : Type.
  Variable w_digits      : positive.
  Variable w_zdigits     : w.
  Variable w_0           : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 08f46aecdc..d9c2340936 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleLift.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_WW : w -> w -> zn2z w.
  Variable w_W0 : w ->  zn2z w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index bc25089729..cc32214017 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleMul.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_1 : w.
  Variable w_WW : w -> w -> zn2z w.
@@ -178,7 +178,7 @@ Section DoubleMul.
  End DoubleMulAddn1.
 
  Section DoubleMulAddmn1.
-  Variable wn: Set.
+  Variable wn: Type.
   Variable extend_n : w -> wn.
   Variable wn_0W : wn -> zn2z wn.
   Variable wn_WW : wn -> wn -> zn2z wn.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 01dd3055f6..00c7aeec65 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleSqrt.
- Variable w              : Set.
+ Variable w              : Type.
  Variable w_is_even      : w -> bool.
  Variable w_compare      : w -> w -> comparison.
  Variable w_0            : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index 9dbfbb4977..638bf69160 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleSub.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_Bm1 : w.
  Variable w_WW : w -> w -> zn2z w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index dfc8b4e32f..73fd266e42 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -19,9 +19,9 @@ Definition base digits := Zpower 2 (Zpos digits).
 
 Section Carry.
 
- Variable A : Set.
+ Variable A : Type.
 
- Inductive carry : Set :=
+ Inductive carry :=
   | C0 : A -> carry
   | C1 : A -> carry.
 
@@ -35,7 +35,7 @@ End Carry.
 
 Section Zn2Z.
 
- Variable znz : Set.
+ Variable znz : Type.
 
  (** From a type [znz] representing a cyclic structure Z/nZ, 
      we produce a representation of Z/2nZ by pairs of elements of [znz]
@@ -43,7 +43,7 @@ Section Zn2Z.
      first. 
  *)
 
- Inductive zn2z : Set :=
+ Inductive zn2z :=
   | W0 : zn2z
   | WW : znz -> znz -> zn2z.
 
@@ -63,7 +63,7 @@ Implicit Arguments W0 [znz].
     (if depth = n). 
 *)
 
-Fixpoint word (w:Set) (n:nat) {struct n} : Set :=
+Fixpoint word (w:Type) (n:nat) : Type :=
  match n with
  | O => w
  | S n => zn2z (word w n)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 5927c2beab..83171388d9 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -17,7 +17,7 @@ Open Scope Z_scope.
 
 Module Type NType.
 
- Parameter t : Set.
+ Parameter t : Type.
  
  Parameter zero : t.
  Parameter one : t.
@@ -101,7 +101,7 @@ End NType.
 
 Module Make (N:NType).
  
- Inductive t_ : Set := 
+ Inductive t_ := 
   | Pos : N.t -> t_
   | Neg : N.t -> t_.
  
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 3f5583927a..facffef45f 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -96,7 +96,7 @@ Notation Local plus_wd := NZplus_wd (only parsing).
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
 
-Definition NZ : Set := Z.
+Definition NZ : Type := Z.
 Definition NZeq := Zeq.
 Definition NZ0 := Z0.
 Definition NZsucc := Zsucc.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 0d3b251f39..ef19069955 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -14,7 +14,7 @@ Require Export NumPrelude.
 
 Module Type NZAxiomsSig.
 
-Parameter Inline NZ : Set.
+Parameter Inline NZ : Type.
 Parameter Inline NZeq : NZ -> NZ -> Prop.
 Parameter Inline NZ0 : NZ.
 Parameter Inline NZsucc : NZ -> NZ.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index b11b840928..f76fa94808 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -370,7 +370,7 @@ Qed.
 safely removed *)
 
 Definition NZsucc_iter (n : nat) (m : NZ) :=
-  nat_rec (fun _ => NZ) m (fun _ l => S l) n.
+  nat_rect (fun _ => NZ) m (fun _ l => S l) n.
 
 Theorem NZlt_succ_iter_r :
   forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 8bd57b9888..a4e8c056fe 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 d15006cb43..ad0bf445cb 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 ed7a7871f4..c3fdd1bf4a 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 c2af667247..170dfa42f2 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 506cf1df07..64f597af0a 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.
diff --git a/theories/Numbers/Rational/BigQ/QMake_base.v b/theories/Numbers/Rational/BigQ/QMake_base.v
index 6c54ed5ad3..da74ee392b 100644
--- a/theories/Numbers/Rational/BigQ/QMake_base.v
+++ b/theories/Numbers/Rational/BigQ/QMake_base.v
@@ -17,7 +17,7 @@ Require Export BigZ.
 
 (* Basic type for Q: a Z or a pair of a Z and an N *)
 
-Inductive q_type : Set := 
+Inductive q_type := 
  | Qz : BigZ.t -> q_type
  | Qq : BigZ.t -> BigN.t -> q_type.
 
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index f47cd4b38a..b05acd7306 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.