- 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

18 files changed, 213 insertions, 252 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index 200d0f7e6..746e7c997 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -8,54 +8,31 @@
 
 (* $Id$ *)
 
-Inductive listT (A:Type) : Type :=
-  | nilT : listT A
-  | consT : A -> listT A -> listT A.
-
-Fixpoint appT (A:Type) (l m:listT A) {struct l} : listT A :=
-  match l with
-  | nilT => m
-  | consT a l1 => consT A a (appT A l1 m)
-  end.
-
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
+Require Import List.
 
 Definition assoc_2nd :=
   (fix assoc_2nd_rec (A:Type) (B:Set)
                      (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
-                     (lst:listT (prodT A B)) {struct lst} : 
+                     (lst:list (prod A B)) {struct lst} : 
    B -> A -> A :=
      fun (key:B) (default:A) =>
        match lst with
-       | nilT => default
-       | consT (pairT v e) l =>
+       | nil => default
+       | (v,e) :: l =>
            match eq_dec e key with
            | left _ => v
            | right _ => assoc_2nd_rec A B eq_dec l key default
            end
        end).
 
-Definition fstT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT a _ => a
-                                            end.
-
-Definition sndT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT _ a => a
-                                            end.
-
 Definition mem :=
   (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) 
-           (a:A) (l:listT A) {struct l} : bool :=
+           (a:A) (l:list A) {struct l} : bool :=
      match l with
-     | nilT => false
-     | consT a1 l1 =>
+     | nil => false
+     | a1 :: l1 =>
          match eq_dec a a1 with
          | left _ => true
          | right _ => mem A eq_dec a l1
          end
      end).
-
-Inductive field_rel_option (A:Type) : Type :=
-  | Field_None : field_rel_option A
-  | Field_Some : (A -> A -> A) -> field_rel_option A.
\ No newline at end of file
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 72306409c..fb6a31e99 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+Require Import List.
 Require Import Ring.
 Require Export Field_Compl.
 Require Export Field_Theory.
@@ -20,8 +21,8 @@ Ltac body_of s := eval cbv beta iota delta [s] in s.
 
 Ltac mem_assoc var lvar :=
   match constr:lvar with
-  | (nilT _) => constr:false
-  | (consT _ ?X1 ?X2) =>
+  | nil => constr:false
+  | ?X1 :: ?X2 =>
       match constr:(X1 = var) with
       | (?X1 = ?X1) => constr:true
       | _ => mem_assoc var X2
@@ -31,10 +32,10 @@ Ltac mem_assoc var lvar :=
 Ltac number lvar := 
   let rec number_aux lvar cpt :=
     match constr:lvar with
-    | (nilT ?X1) => constr:(nilT (prodT X1 nat))
-    | (consT ?X1 ?X2 ?X3) =>
+    | (@nil ?X1) => constr:(@nil (prod X1 nat))
+    | ?X2 :: ?X3 =>
         let l2 := number_aux X3 (S cpt) in
-        constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2) 
+        constr:((X2,cpt) :: l2) 
     end
   in number_aux lvar 0.
 
@@ -62,17 +63,17 @@ Ltac build_varlist FT trm :=
         let res := mem_assoc X1 lvar in
         match constr:res with
         | true => lvar
-        | false => constr:(consT AT X1 lvar)
+        | false => constr:(X1 :: lvar)
         end
     end in
   let AT := get_component A FT in
-  let lvar := seek_var (nilT AT) trm in
+  let lvar := seek_var (@nil AT) trm in
   number lvar.
 
 Ltac assoc elt lst :=
   match constr:lst with
-  | (nilT _) => fail
-  | (consT (prodT _ nat) (pairT _ nat ?X1 ?X2) ?X3) =>
+  | nil => fail
+  | (?X1,?X2) :: ?X3 =>
       match constr:(elt = X1) with
       | (?X1 = ?X1) => constr:X2
       | _ => assoc elt X3
@@ -113,32 +114,31 @@ Ltac interp_A FT lvar trm :=
 
 Ltac remove e l :=
   match constr:l with
-  | (nilT _) => l
-  | (consT ?X1 e ?X2) => constr:X2
-  | (consT ?X1 ?X2 ?X3) => let nl := remove e X3 in
-                           constr:(consT X1 X2 nl)
+  | nil => l
+  | e :: ?X2 => constr:X2
+  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
   end.
 
 Ltac union l1 l2 :=
   match constr:l1 with
-  | (nilT _) => l2
-  | (consT ?X1 ?X2 ?X3) =>
+  | nil => l2
+  | ?X2 :: ?X3 =>
       let nl2 := remove X2 l2 in
       let nl := union X3 nl2 in
-      constr:(consT X1 X2 nl)
+      constr:(X2 :: nl)
   end.
 
 Ltac raw_give_mult trm :=
   match constr:trm with
-  | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA))
+  | (EAinv ?X1) => constr:(X1 :: nil)
   | (EAopp ?X1) => raw_give_mult X1
   | (EAplus ?X1 ?X2) =>
       let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
       union l1 l2
   | (EAmult ?X1 ?X2) =>
       let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
-      eval compute in (appT ExprA l1 l2)
-  | _ => constr:(nilT ExprA)
+      eval compute in (app l1 l2)
+  | _ => constr:(@nil ExprA)
   end.
 
 Ltac give_mult trm :=
@@ -254,13 +254,13 @@ Ltac apply_simplif sfun :=
 
 Ltac unfolds FT :=
   match get_component Aminus FT with
-  | (Field_Some _ ?X1) => unfold X1 in |- *
+  | Some ?X1 => unfold X1 in |- *
   | _ => idtac
   end;
-   match get_component Adiv FT with
-   | (Field_Some _ ?X1) => unfold X1 in |- *
-   | _ => idtac
-   end.
+  match get_component Adiv FT with
+  | Some ?X1 => unfold X1 in |- *
+  | _ => idtac
+  end.
 
 Ltac reduce FT :=
   let AzeroT := get_component Azero FT
@@ -304,11 +304,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
 Ltac init_exp FT trm :=
   let e :=
    (match get_component Aminus FT with
-    | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
+    | Some ?X1 => eval cbv beta delta [X1] in trm
     | _ => trm
     end) in
   match get_component Adiv FT with
-  | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
+  | Some ?X1 => eval cbv beta delta [X1] in e
   | _ => e
   end.
 
@@ -341,21 +341,21 @@ Ltac simpl_inv trm :=
 
 Ltac map_tactic fcn lst :=
   match constr:lst with
-  | (nilT _) => lst
-  | (consT ?X1 ?X2 ?X3) =>
+  | nil => lst
+  | ?X2 :: ?X3 =>
       let r := fcn X2 with t := map_tactic fcn X3 in
-      constr:(consT X1 r t)
+      constr:(r :: t)
   end.
 
 Ltac build_monom_aux lst trm :=
   match constr:lst with
-  | (nilT _) => eval compute in (assoc trm)
-  | (consT _ ?X1 ?X2) => build_monom_aux X2 (EAmult trm X1)
+  | nil => eval compute in (assoc trm)
+  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
   end.
 
 Ltac build_monom lnum lden :=
   let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
-  let ltot := eval compute in (appT ExprA lnum ildn) in
+  let ltot := eval compute in (app lnum ildn) in
   let trm := build_monom_aux ltot EAone in
   match constr:trm with
   | (EAmult _ ?X1) => constr:X1
@@ -370,7 +370,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlnum := remove X1 lnum in
           simpl_monom_aux newlnum lden X2
-      | false => simpl_monom_aux lnum (consT ExprA X1 lden) X2
+      | false => simpl_monom_aux lnum (X1 :: lden) X2
       end
   | (EAmult ?X1 ?X2) =>
       let mma := mem_assoc X1 lden in
@@ -378,7 +378,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlden := remove X1 lden in
           simpl_monom_aux lnum newlden X2
-      | false => simpl_monom_aux (consT ExprA X1 lnum) lden X2
+      | false => simpl_monom_aux (X1 :: lnum) lden X2
       end
   | (EAinv ?X1) =>
       let mma := mem_assoc X1 lnum in
@@ -386,7 +386,7 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlnum := remove X1 lnum in
           build_monom newlnum lden
-      | false => build_monom lnum (consT ExprA X1 lden)
+      | false => build_monom lnum (X1 :: lden)
       end
   | ?X1 =>
       let mma := mem_assoc X1 lden in
@@ -394,11 +394,11 @@ Ltac simpl_monom_aux lnum lden trm :=
       | true =>
           let newlden := remove X1 lden in
           build_monom lnum newlden
-      | false => build_monom (consT ExprA X1 lnum) lden
+      | false => build_monom (X1 :: lnum) lden
       end
   end.
 
-Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT ExprA) trm.
+Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
 
 Ltac simpl_all_monomials trm :=
   match constr:trm with
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 7fdf61bb4..5fe69ddca 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+Require Import List.
 Require Import Peano_dec.
 Require Import Ring.
 Require Import Field_Compl.
@@ -21,8 +22,8 @@ Record Field_Theory : Type :=
    Aopp : A -> A;
    Aeq : A -> A -> bool;
    Ainv : A -> A;
-   Aminus : field_rel_option A;
-   Adiv : field_rel_option A;
+   Aminus : option (A -> A -> A);
+   Adiv : option (A -> A -> A);
    RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
    Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
 
@@ -66,10 +67,10 @@ Definition eqExprA := Eval compute in eqExprA_O.
 
 (**** Generation of the multiplier ****)
 
-Fixpoint mult_of_list (e:listT ExprA) : ExprA :=
+Fixpoint mult_of_list (e:list ExprA) : ExprA :=
   match e with
-  | nilT => EAone
-  | consT e1 l1 => EAmult e1 (mult_of_list l1)
+  | nil => EAone
+  | e1 :: l1 => EAmult e1 (mult_of_list l1)
   end.
 
 Section Theory_of_fields.
@@ -191,7 +192,7 @@ Qed.
 
 (**** ExprA --> A ****)
 
-Fixpoint interp_ExprA (lvar:listT (prodT AT nat)) (e:ExprA) {struct e} :
+Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
  AT :=
   match e with
   | EAzero => AzeroT
@@ -257,7 +258,7 @@ Fixpoint assoc (e:ExprA) : ExprA :=
   end.
 
 Lemma merge_mult_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
    interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).
 Proof.
@@ -271,7 +272,7 @@ unfold merge_mult at 1 in |- *; fold merge_mult in |- *;
 Qed.
 
 Lemma merge_mult_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
 Proof.
 simple induction e1; auto; intros.
@@ -290,7 +291,7 @@ ring.
 Qed.
 
 Lemma assoc_mult_correct1 :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    AmultT (interp_ExprA lvar (assoc_mult e1))
      (interp_ExprA lvar (assoc_mult e2)) =
    interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
@@ -302,7 +303,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
 Qed.
 
 Lemma assoc_mult_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
 Proof.
 simple induction e; auto; intros.
@@ -325,7 +326,7 @@ simpl in |- *; rewrite (H0 lvar); auto.
 Qed.
 
 Lemma merge_plus_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
    interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).
 Proof.
@@ -339,7 +340,7 @@ unfold merge_plus at 1 in |- *; fold merge_plus in |- *;
 Qed.
 
 Lemma merge_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
 Proof.
 simple induction e1; auto; intros.
@@ -358,7 +359,7 @@ ring.
 Qed.
 
 Lemma assoc_plus_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
    interp_ExprA lvar (assoc (EAplus e1 e2)).
 Proof.
@@ -369,7 +370,7 @@ rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
 Qed.
 
 Lemma assoc_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
 Proof.
 simple induction e; auto; intros.
@@ -448,7 +449,7 @@ Fixpoint distrib_main (e:ExprA) : ExprA :=
 Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
 
 Lemma distrib_mult_right_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib_mult_right e1 e2) =
    AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 Proof.
@@ -458,7 +459,7 @@ rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
 Qed.
 
 Lemma distrib_mult_left_correct :
- forall (e1 e2:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib_mult_left e1 e2) =
    AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
 Proof.
@@ -480,7 +481,7 @@ rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
 Qed.
 
 Lemma distrib_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
 Proof.
 simple induction e; intros; auto.
@@ -496,7 +497,7 @@ Qed.
 (**** Multiplication by the inverse product ****)
 
 Lemma mult_eq :
- forall (e1 e2 a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e1 e2 a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) ->
    interp_ExprA lvar e1 = interp_ExprA lvar e2.
@@ -520,7 +521,7 @@ Definition multiply (e:ExprA) : ExprA :=
   end.
 
 Lemma multiply_aux_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (a e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (multiply_aux a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
 Proof.
@@ -530,7 +531,7 @@ simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
 Qed.
 
 Lemma multiply_correct :
- forall (e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
 Proof.
   simple induction e; simpl in |- *; auto.
@@ -578,7 +579,7 @@ Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
   end.
 
 Lemma monom_remove_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_remove a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
@@ -608,7 +609,7 @@ unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
 Qed.
 
 Lemma monom_simplif_rem_correct :
- forall (a e:ExprA) (lvar:listT (prodT AT nat)),
+ forall (a e:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_simplif_rem a e) =
    AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
@@ -622,7 +623,7 @@ ring.
 Qed.
 
 Lemma monom_simplif_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
 Proof.
@@ -633,7 +634,7 @@ simpl in |- *; trivial.
 Qed.
 
 Lemma inverse_correct :
- forall (e a:ExprA) (lvar:listT (prodT AT nat)),
+ forall (e a:ExprA) (lvar:list (AT * nat)),
    interp_ExprA lvar a <> AzeroT ->
    interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
 Proof.
@@ -642,4 +643,4 @@ simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
 unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto.
 Qed.
 
-End Theory_of_fields.
\ No newline at end of file
+End Theory_of_fields.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 90a986385..8e33f6292 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -22,19 +22,22 @@ open Vernacinterp
 open Vernacexpr
 open Tacexpr
 open Mod_subst
+open Coqlib
 
 (* Interpretation of constr's *)
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 (* Construction of constants *)
-let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s
+let constant dir s = gen_constant "Field" ("field"::dir) s
+let init_constant s = gen_constant_in_modules "Field" init_modules s
 
 (* To deal with the optional arguments *)
 let constr_of_opt a opt =
   let ac = constr_of a in
+  let ac3 = mkArrow ac (mkArrow ac ac) in
   match opt with
-  | None -> mkApp ((constant ["Field_Compl"] "Field_None"),[|ac|])
-  | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|])
+  | None -> mkApp (init_constant "None",[|ac3|])
+  | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
 
 (* Table of theories *)
 let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index f9a1c6466..cfde10202 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -152,12 +152,7 @@ type coq_sigma_data = {
 
 type 'a delayed = unit -> 'a
 
-let build_sigma_set () =
-  { proj1 = init_constant ["Specif"] "projS1";
-    proj2 = init_constant ["Specif"] "projS2";
-    elim = init_constant ["Specif"] "sigS_rec";
-    intro = init_constant ["Specif"] "existS";
-    typ = init_constant ["Specif"] "sigS" }
+let build_sigma_set () = anomaly "Use build_sigma_type"
 
 let build_sigma_type () =
   { proj1 = init_constant ["Specif"] "projT1";
@@ -257,7 +252,7 @@ let build_coq_ex ()   = Lazy.force coq_ex
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref     = lazy (init_reference ["Datatypes"] "identity")
-let coq_existS_ref  = lazy (init_reference ["Specif"] "existS")
+let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
 let coq_False_ref   = lazy (init_reference ["Logic"] "False")
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6239879c9..34cfefd5d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -547,8 +547,7 @@ let discrHyp id gls = discrClause (onHyp id) gls
 
 let find_sigma_data s =
   match s with  
-    | Prop Pos  -> build_sigma_set ()                    (* Set *) 
-    | Type _    -> build_sigma_type ()                   (* Type *)
+    | Prop Pos  | Type _    -> build_sigma_type ()          (* Set/Type *)
     | Prop Null -> error "find_sigma_data"
 
 (* [make_tuple env sigma (rterm,rty) lind] assumes [lind] is the lesser
@@ -556,7 +555,7 @@ let find_sigma_data s =
 
    Then we build the term
 
-     [(existS A P (mkRel lind) rterm)] of type [(sigS A P)]
+     [(existT A P (mkRel lind) rterm)] of type [(sigS A P)]
 
    where [A] is the type of [mkRel lind] and [P] is [\na:A.rty{1/lind}]
  *)
@@ -687,7 +686,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the
    tuple
 
-   [existS [xn]Pn Rel(in) .. (existS [x2]P2 Rel(i2) (existS [x1]P1 Rel(i1) z))]
+   [existT [xn]Pn Rel(in) .. (existT [x2]P2 Rel(i2) (existT [x1]P1 Rel(i1) z))]
 
    where P1 is zty[i1/x1], P2 is {x1 | P1[i2/x2]} etc.
 
@@ -702,7 +701,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    need also to construct a default value for the other branches of
    the destructor. As default value, we take a tuple of the form
 
-    [existS [xn]Pn ?n (... existS [x2]P2 ?2 (existS [x1]P1 ?1 term))]
+    [existT [xn]Pn ?n (... existT [x2]P2 ?2 (existT [x1]P1 ?1 term))]
 
    but for this we have to solve the following unification problem:
 
@@ -917,7 +916,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
    Given that dep_pair looks like:
 
-   (existS e1 (existS e2 ... (existS en en+1) ... ))
+   (existT e1 (existT e2 ... (existT en en+1) ... ))
 
    and B might contain instances of the ei, we will return the term:
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index e35623b52..302d9a992 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -279,7 +279,6 @@ let dest_nf_eq gls eqn =
 
 (* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
 let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
 let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
 
 let match_sigma ex ex_pat =
@@ -292,8 +291,7 @@ let match_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex) 
-    [coq_existS_pattern, build_sigma_set; 
-     coq_existT_pattern, build_sigma_type]
+    [coq_existT_pattern, build_sigma_type]
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 67040c15d..6dde098cf 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -101,7 +101,7 @@ open Coqlib
 val find_eq_data_decompose : constr -> 
   coq_leibniz_eq_data * (constr * constr * constr)
 
-(* Match a term of the form [(existS A P t p)] or [(existT A P t p)] *)
+(* Match a term of the form [(existT A P t p)] *)
 (* Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : constr -> 
   coq_sigma_data * (constr * constr * constr * constr)
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.