Passage de Set à Type dans Relations et Wellfounded

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

1 files changed, 8 insertions, 11 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index b45aa23fe..3c276cd2b 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -242,7 +242,7 @@ End DecidableEqDep.
 
 Module Type DecidableSet.
 
-  Parameter U:Set.
+  Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableSet.
@@ -283,14 +283,6 @@ Module DecidableEqDepSet (M:DecidableSet).
     forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
   Proof N.Streicher_K.
 
-  (** Injectivity of equality on dependent pairs with second component
-      in [Type] *)
-
-  Lemma inj_pairT2 :
-    forall (P:U -> Type) (p:U) (x y:P p),
-      existT P p x = existT P p y -> x = y.
-  Proof N.inj_pairT2.
-
   (** Proof-irrelevance on subsets of decidable sets *)
 
   Lemma inj_pairP2 :
@@ -298,11 +290,16 @@ Module DecidableEqDepSet (M:DecidableSet).
       ex_intro P x p = ex_intro P x q -> p = q.
   Proof N.inj_pairP2.
 
-  (** Injectivity of equality on dependent pairs in [Set] *)
+  (** Injectivity of equality on dependent pairs in [Type] *)
 
   Lemma inj_pair2 :
-    forall (P:U -> Set) (p:U) (x y:P p),
+    forall (P:U -> Type) (p:U) (x y:P p),
       existS P p x = existS P p y -> x = y.
   Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
 
+  (** Injectivity of equality on dependent pairs with second component
+      in [Type] *)
+
+  Notation inj_pairT2 := inj_pair2.
+
 End DecidableEqDepSet.