- Déplacement des types paramétriques prod, sum, option, identity,

  sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
  ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field


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

10 files changed, 128 insertions, 140 deletions

diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index eafc1fabb..1c965c7e0 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -46,9 +46,9 @@ Une fonction binaire sur A génère une fonction des couple de vecteurs
 de taille n dans les vecteurs de taille n en appliquant f terme à terme.
 *)
 
-Variable A : Set.
+Variable A : Type.
 
-Inductive vector : nat -> Set :=
+Inductive vector : nat -> Type :=
   | Vnil : vector 0
   | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
 
@@ -59,7 +59,7 @@ Defined.
 
 Definition Vtail : forall n:nat, vector (S n) -> vector n.
 Proof.
-	intros n v; inversion v; exact H0.
+	intros n v; inversion v as [|_ n0 H0 H1]; exact H0.
 Defined.
 
 Definition Vlast : forall n:nat, vector (S n) -> A.
@@ -68,7 +68,7 @@ Proof.
 	inversion v.
 	exact a.
 
-	inversion v.
+	inversion v as [| n0 a H0 H1].
 	exact (f H0).
 Defined.
 
@@ -85,7 +85,7 @@ Proof.
 	induction n as [| n f]; intro v.
 	exact Vnil.
 
-	inversion v.
+	inversion v as [| a n0 H0 H1].
 	exact (Vcons a n (f H0)).
 Defined.
 
@@ -94,7 +94,7 @@ Proof.
 	induction n as [| n f]; intros a v.
 	exact (Vcons a 0 v).
 
-	inversion v.
+	inversion v as [| a0 n0 H0 H1 ].
 	exact (Vcons a (S n) (f a H0)).
 Defined.
 
@@ -104,7 +104,7 @@ Proof.
 	inversion v.
 	exact (Vcons a 1 v).
 
-	inversion v.
+	inversion v as [| a n0 H0 H1 ].
 	exact (Vcons a (S (S n)) (f H0)).
 Defined.
 
@@ -128,7 +128,7 @@ Proof.
 	induction n as [| n f]; intros p v v0.
 	simpl in |- *; exact v0.
 
-	inversion v.
+	inversion v as [| a n0 H0 H1].
 	simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
 Defined.
 
@@ -139,7 +139,7 @@ Proof.
 	induction n as [| n g]; intro v.
 	exact Vnil.
 
-	inversion v.
+	inversion v as [| a n0 H0 H1].
 	exact (Vcons (f a) n (g H0)).
 Defined.
 
@@ -150,15 +150,15 @@ Proof.
 	induction n as [| n h]; intros v v0.
 	exact Vnil.
 
-	inversion v; inversion v0.
+	inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
 	exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
 
 Definition Vid : forall n:nat, vector n -> vector n.
 Proof.
-destruct n; intros.
+destruct n; intro X.
 exact Vnil.
-exact (Vcons (Vhead _ H) _ (Vtail _ H)).
+exact (Vcons (Vhead _ X) _ (Vtail _ X)).
 Defined.
 
 Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v).
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 7fa518d66..82363fff7 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -10,7 +10,7 @@
 
 Set Implicit Arguments.
 
-Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
+Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
   if H then x else y.
 
 
@@ -28,4 +28,4 @@ intros; case H; auto.
 intro; absurd A; trivial.
 Qed.
 
-Unset Implicit Arguments.
\ No newline at end of file
+Unset Implicit Arguments.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 369fd2cbd..6ec194325 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -47,7 +47,7 @@ Inductive Empty_set : Set :=.
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [refl_identity A a] *)
 
-Inductive identity (A:Type) (a:A) : A -> Set :=
+Inductive identity (A:Type) (a:A) : A -> Type :=
     refl_identity : identity (A:=A) a a.
 Hint Resolve refl_identity: core v62.
 
@@ -57,13 +57,13 @@ Implicit Arguments identity_rect [A].
 
 (** [option A] is the extension of [A] with an extra element [None] *)
 
-Inductive option (A:Set) : Set :=
+Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
 Implicit Arguments None [A].
 
-Definition option_map (A B:Set) (f:A->B) o :=
+Definition option_map (A B:Type) (f:A->B) o :=
   match o with
   | Some a => Some (f a)
   | None => None
@@ -71,7 +71,7 @@ Definition option_map (A B:Set) (f:A->B) o :=
 
 (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
-Inductive sum (A B:Set) : Set :=
+Inductive sum (A B:Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
 
@@ -80,7 +80,7 @@ Notation "x + y" := (sum x y) : type_scope.
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 
-Inductive prod (A B:Set) : Set :=
+Inductive prod (A B:Type) : Type :=
     pair : A -> B -> prod A B.
 Add Printing Let prod.
 
@@ -88,31 +88,38 @@ Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
 Section projections.
-   Variables A B : Set.
-   Definition fst (p:A * B) := match p with
-                               | (x, y) => x
-                               end.
-   Definition snd (p:A * B) := match p with
-                               | (x, y) => y
-                               end.
+  Variables A B : Type.
+  Definition fst (p:A * B) := match p with
+                              | (x, y) => x
+                              end.
+  Definition snd (p:A * B) := match p with
+                              | (x, y) => y
+                              end.
 End projections. 
 
 Hint Resolve pair inl inr: core v62.
 
 Lemma surjective_pairing :
- forall (A B:Set) (p:A * B), p = pair (fst p) (snd p).
+ forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
 Proof.
 destruct p; reflexivity.
 Qed.
 
 Lemma injective_projections :
- forall (A B:Set) (p1 p2:A * B),
+ forall (A B:Type) (p1 p2:A * B),
    fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
 destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
 rewrite Hfst; rewrite Hsnd; reflexivity. 
 Qed.
 
+Definition prod_uncurry (A B C:Type) (f:prod A B -> C) 
+  (x:A) (y:B) : C := f (pair x y).
+
+Definition prod_curry (A B C:Type) (f:A -> B -> C) 
+  (p:prod A B) : C := match p with
+                       | pair x y => f x y
+                       end.
 
 (** Comparison *)
 
@@ -127,3 +134,12 @@ Definition CompOpp (r:comparison) :=
   | Lt => Gt
   | Gt => Lt
   end.
+
+(* Compatibility *)
+
+Notation prodT := prod (only parsing).
+Notation pairT := pair (only parsing).
+Notation fstT := fst (only parsing).
+Notation sndT := snd (only parsing).
+Notation prodT_uncurry := prod_uncurry (only parsing).
+Notation prodT_curry := prod_curry (only parsing).
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 464c8071d..faeecdf9d 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -20,32 +20,6 @@ Require Export Logic.
 
 Definition notT (A:Type) := A -> False.
 
-(** Conjunction of types in [Type] *)
-
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
-
-Section prodT_proj.
-
-  Variables A B : Type.
-
-  Definition fstT (H:prodT A B) := match H with
-                                   | pairT x _ => x
-                                   end.
-  Definition sndT (H:prodT A B) := match H with
-                                   | pairT _ y => y
-                                   end.
-
-End prodT_proj.
-
-Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
-  (x:A) (y:B) : C := f (pairT x y).
-
-Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
-  (p:prodT A B) : C := match p with
-                       | pairT x y => f x y
-                       end.
-
 (** Properties of [identity] *)
 
 Section identity_is_a_congruence.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index fe24706e4..ffbf83d80 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -62,6 +62,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
 
 (** Notations for sigma-types or subsets *)
 
+Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
+Reserved Notation "{ x  |  P  &  Q }" (at level 0, x at level 99).
+
 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index f42749293..5bf9621b1 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -19,42 +19,45 @@ Require Import Logic.
 (** Subsets and Sigma-types *)
 
 (** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset 
-    of elements of the Set [A] which satisfy the predicate [P].
+    of elements of the type [A] which satisfy the predicate [P].
     Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset 
-    of elements of the Set [A] which satisfy both [P] and [Q]. *)
+    of elements of the type [A] which satisfy both [P] and [Q]. *)
 
-Inductive sig (A:Set) (P:A -> Prop) : Set :=
-    exist : forall x:A, P x -> sig (A:=A) P.
+Inductive sig (A:Type) (P:A -> Prop) : Type :=
+    exist : forall x:A, P x -> sig P.
 
-Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
-    exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q.
+Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
+    exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
-(** [(sigS A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. 
-    It is a variant of subset where [P] is now of type [Set].
-    Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
-     
-Inductive sigS (A:Set) (P:A -> Set) : Set :=
-    existS : forall x:A, P x -> sigS (A:=A) P.
+(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. 
+    Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
-Inductive sigS2 (A:Set) (P Q:A -> Set) : Set :=
-    existS2 : forall x:A, P x -> Q x -> sigS2 (A:=A) P Q.
+Inductive sigT (A:Type) (P:A -> Type) : Type :=
+    existT : forall x:A, P x -> sigT P.
+
+Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
+    existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
+
+(* Notations *)
 
 Arguments Scope sig [type_scope type_scope].
 Arguments Scope sig2 [type_scope type_scope type_scope].
-Arguments Scope sigS [type_scope type_scope].
-Arguments Scope sigS2 [type_scope type_scope type_scope].
+Arguments Scope sigT [type_scope type_scope].
+Arguments Scope sigT2 [type_scope type_scope type_scope].
 
+Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
+Notation "{ x  |  P  &  Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
 Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
 Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
   type_scope.
-Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
-Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
+Notation "{ x : A  &  P }" := (sigT (fun x:A => P)) : type_scope.
+Notation "{ x : A  &  P  &  Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :
   type_scope.
 
 Add Printing Let sig.
 Add Printing Let sig2.
-Add Printing Let sigS.
-Add Printing Let sigS2.
+Add Printing Let sigT.
+Add Printing Let sigT2.
 
 
 (** Projections of [sig]
@@ -67,7 +70,7 @@ Add Printing Let sigS2.
 
 Section Subset_projections.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable P : A -> Prop.
 
   Definition proj1_sig (e:sig P) := match e with
@@ -82,24 +85,24 @@ Section Subset_projections.
 End Subset_projections.
 
 
-(** Projections of [sigS]
+(** Projections of [sigT]
 
     An element [x] of a sigma-type [{y:A & P y}] is a dependent pair
     made of an [a] of type [A] and an [h] of type [P a].  Then,
-    [(projS1 x)] is the first projection and [(projS2 x)] is the
-    second projection, the type of which depends on the [projS1]. *)
+    [(projT1 x)] is the first projection and [(projT2 x)] is the
+    second projection, the type of which depends on the [projT1]. *)
 
 Section Projections.
 
-  Variable A : Set.
-  Variable P : A -> Set.
+  Variable A : Type.
+  Variable P : A -> Type.
 
-  Definition projS1 (x:sigS P) : A := match x with
-                                      | existS a _ => a
+  Definition projT1 (x:sigT P) : A := match x with
+                                      | existT a _ => a
                                       end.
-  Definition projS2 (x:sigS P) : P (projS1 x) :=
-    match x return P (projS1 x) with
-    | existS _ h => h
+  Definition projT2 (x:sigT P) : P (projT1 x) :=
+    match x return P (projT1 x) with
+    | existT _ h => h
     end.
 
 End Projections.
@@ -118,7 +121,7 @@ Add Printing If sumbool.
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
-Inductive sumor (A:Set) (B:Prop) : Set :=
+Inductive sumor (A:Type) (B:Prop) : Type :=
   | inleft : A -> A + {B}
   | inright : B -> A + {B} 
  where "A + { B }" := (sumor A B) : type_scope.
@@ -146,12 +149,12 @@ Section Choice_lemmas.
   Qed.
 
   Lemma Choice2 :
-   (forall x:S, sigS (fun y:S' => R' x y)) ->
-   sigS (fun f:S -> S' => forall z:S, R' z (f z)).
+   (forall x:S, sigT (fun y:S' => R' x y)) ->
+   sigT (fun f:S -> S' => forall z:S, R' z (f z)).
   Proof.
     intro H.
     exists (fun z:S => match H z with
-                       | existS y _ => y
+                       | existT y _ => y
                        end).
     intro z; destruct (H z); trivial.
   Qed.
@@ -176,7 +179,7 @@ End Choice_lemmas.
  (** A result of type [(Exc A)] is either a normal value of type [A] or 
      an [error] :
 
-     [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)].
+     [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
 
      It is implemented using the option type. *) 
 
@@ -199,24 +202,18 @@ Qed.
 
 Hint Resolve left right inleft inright: core v62.
 
-(** Sigma-type for types in [Type] *)
-
-Inductive sigT (A:Type) (P:A -> Type) : Type :=
-    existT : forall x:A, P x -> sigT (A:=A) P.
-
-Section projections_sigT.
-
-  Variable A : Type.
-  Variable P : A -> Type.
-
-  Definition projT1 (H:sigT P) : A := match H with
-                                      | existT x _ => x
-                                      end.
-   
-  Definition projT2 : forall x:sigT P, P (projT1 x) :=
-    fun H:sigT P => match H return P (projT1 H) with
-                    | existT x h => h
-                    end.
-
-End projections_sigT.
-
+(* Compatibility *)
+
+Notation sigS := sigT (only parsing).
+Notation existS := existT (only parsing).
+Notation sigS_rect := sigT_rect (only parsing).
+Notation sigS_rec := sigT_rec (only parsing).
+Notation sigS_ind := sigT_ind (only parsing).
+Notation projS1 := projT1 (only parsing).
+Notation projS2 := projT2 (only parsing).
+
+Notation sigS2 := sigT2 (only parsing).
+Notation existS2 := existT2 (only parsing).
+Notation sigS2_rect := sigT2_rect (only parsing).
+Notation sigS2_rec := sigT2_rec (only parsing).
+Notation sigS2_ind := sigT2_ind (only parsing).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 79d5a95b0..ffe3ac533 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -22,9 +22,9 @@ Set Implicit Arguments.
 
 Section Lists.
 
-  Variable A : Set.
+  Variable A : Type.
 
-  Inductive list : Set :=
+  Inductive list : Type :=
     | nil : list
     | cons : A -> list -> list.
 
@@ -90,7 +90,7 @@ Bind Scope list_scope with list.
 
 Section Facts.
 
-  Variable A : Set.
+  Variable A : Type.
 
 
   (** *** Genereric facts *)
@@ -168,7 +168,7 @@ Section Facts.
     (forall x y:A, {x = y} + {x <> y}) ->
     forall (a:A) (l:list A), {In a l} + {~ In a l}.
   Proof.
-    induction l as [| a0 l IHl].
+    intro H; induction l as [| a0 l IHl].
     right; apply in_nil.
     destruct (H a0 a); simpl in |- *; auto.
     destruct IHl; simpl in |- *; auto. 
@@ -332,7 +332,7 @@ Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
 
 Section Elts.
 
-  Variable A : Set.
+  Variable A : Type.
 
   (*****************************)
   (** ** Nth element of a list *)
@@ -582,7 +582,7 @@ End Elts.
 
 Section ListOps.
 
-  Variable A : Set.
+  Variable A : Type.
 
   (*************************)
   (** ** Reverse           *)
@@ -988,7 +988,7 @@ End ListOps.
 (************)
 
 Section Map.
-  Variables A B : Set.
+  Variables A B : Type.
   Variable f : A -> B.
   
   Fixpoint map (l:list A) : list B :=
@@ -1071,7 +1071,7 @@ Section Map.
 
 End Map. 
 
-Lemma map_map : forall (A B C:Set)(f:A->B)(g:B->C) l, 
+Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, 
   map g (map f l) = map (fun x => g (f x)) l.
 Proof.
   induction l; simpl; auto.
@@ -1079,7 +1079,7 @@ Proof.
 Qed.
 
 Lemma map_ext : 
-  forall (A B : Set)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
+  forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
 Proof.
   induction l; simpl; auto.
   rewrite H; rewrite IHl; auto.
@@ -1091,7 +1091,7 @@ Qed.
 (************************************)
 
 Section Fold_Left_Recursor.
-  Variables A B : Set.
+  Variables A B : Type.
   Variable f : A -> B -> A.
   
   Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
@@ -1113,7 +1113,7 @@ Section Fold_Left_Recursor.
 End Fold_Left_Recursor.
 
 Lemma fold_left_length : 
-  forall (A:Set)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
+  forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
 Proof.
   intro A.
   cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l).
@@ -1129,7 +1129,7 @@ Qed.
 (************************************)
 
 Section Fold_Right_Recursor.
-  Variables A B : Set.
+  Variables A B : Type.
   Variable f : B -> A -> A.
   Variable a0 : A.
   
@@ -1141,7 +1141,7 @@ Section Fold_Right_Recursor.
 
 End Fold_Right_Recursor.
 
-  Lemma fold_right_app : forall (A B:Set)(f:A->B->B) l l' i, 
+  Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, 
     fold_right f i (l++l') = fold_right f (fold_right f i l') l.
   Proof.
     induction l.
@@ -1150,7 +1150,7 @@ End Fold_Right_Recursor.
     f_equal; auto.
   Qed.
 
-  Lemma fold_left_rev_right : forall (A B:Set)(f:A->B->B) l i, 
+  Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, 
     fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
   Proof.
     induction l.
@@ -1161,7 +1161,7 @@ End Fold_Right_Recursor.
   Qed.
 
   Theorem fold_symmetric :
-    forall (A:Set) (f:A -> A -> A),
+    forall (A:Type) (f:A -> A -> A),
       (forall x y z:A, f x (f y z) = f (f x y) z) ->
       (forall x y:A, f x y = f y x) ->
       forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.
@@ -1187,7 +1187,7 @@ End Fold_Right_Recursor.
   (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
       indexed by elts of [x], sorted in lexicographic order. *)
 
-  Fixpoint list_power (A B:Set)(l:list A) (l':list B) {struct l} :
+  Fixpoint list_power (A B:Type)(l:list A) (l':list B) {struct l} :
     list (list (A * B)) :=
     match l with
       | nil => cons nil nil
@@ -1202,7 +1202,7 @@ End Fold_Right_Recursor.
   (*************************************)
 
   Section Bool. 
-    Variable A : Set.
+    Variable A : Type.
     Variable f : A -> bool.
 
   (** find whether a boolean function can be satisfied by an 
@@ -1301,7 +1301,7 @@ End Fold_Right_Recursor.
   (******************************************************)
 
   Section ListPairs.
-    Variables A B : Set.
+    Variables A B : Type.
     
   (** [split] derives two lists from a list of pairs *)
 
@@ -1495,7 +1495,7 @@ End Fold_Right_Recursor.
 (******************************)
 
 Section length_order.
-  Variable A : Set.
+  Variable A : Type.
 
   Definition lel (l m:list A) := length l <= length m.
 
@@ -1548,7 +1548,7 @@ Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
 
 Section SetIncl.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
   Hint Unfold incl.
@@ -1617,7 +1617,7 @@ Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
 
 Section Cutting.
 
-  Variable A : Set.
+  Variable A : Type.
 
   Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := 
     match n with 
@@ -1654,7 +1654,7 @@ End Cutting.
 
 Section ReDun.
 
-  Variable A : Set.
+  Variable A : Type.
   
   Inductive NoDup : list A -> Prop := 
     | NoDup_nil : NoDup nil 
@@ -1777,5 +1777,3 @@ Hint Rewrite <-
 
 Ltac simpl_list := autorewrite with list.
 Ltac ssimpl_list := autorewrite with list using simpl.
-
-
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 26eae1a05..226d07149 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -14,7 +14,7 @@ Require Export List.
 Set Implicit Arguments.
 Section Lists.
 
-Variable A : Set.
+Variable A : Type.
 
 (**********************)
 (** The null function *)
@@ -325,7 +325,7 @@ Realizer find.
 *)
 Qed.
 
-Variable B : Set.
+Variable B : Type.
 Variable T : A -> B -> Prop.
 
 Variable TS_dec : forall a:A, {c : B | T a c} + {P a}.
@@ -358,7 +358,7 @@ End Find_sec.
 
 Section Assoc_sec.
 
-Variable B : Set.
+Variable B : Type.
 Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : 
  Exc B :=
   match l with
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 9496099a8..884f05e52 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -339,7 +339,7 @@ with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Typ
 Definition product_of_arguments : Arguments -> Type.
  induction 1.
    exact (carrier_of_relation_class a).
-   exact (prodT (carrier_of_relation_class a) IHX).
+   exact (prod (carrier_of_relation_class a) IHX).
 Defined.
 
 Definition get_rewrite_direction: rewrite_direction -> Argument_Class -> rewrite_direction.
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 714abfc45..4003c3389 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -383,7 +383,7 @@ Qed.
 (** Reverting [x ?= y] to trichotomy *)
 
 Lemma rename :
- forall (A:Set) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x.
+ forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x.
 Proof.
 auto with arith. 
 Qed.