From 4da13b45ea2da8525c7f2dc38833cf24f6f02e74 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Oct 2014 10:56:15 +0200
Subject: EqdepFacts: generalize statements which were wrongly restricted to
 Prop.

---
 theories/Logic/EqdepFacts.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index afd0ecf046..939fbe408a 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -142,7 +142,7 @@ Qed.
 Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *)
 
 Lemma eq_sig_eq_dep :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     exist P p x = exist P q y -> eq_dep p x q y.
 Proof.
   intros.
@@ -151,14 +151,14 @@ Proof.
 Qed.
 
 Lemma eq_dep_eq_sig :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     eq_dep p x q y -> exist P p x = exist P q y.
 Proof.
   destruct 1; reflexivity.
 Qed.
 
 Lemma eq_sig_iff_eq_dep :
-  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
     exist P p x = exist P q y <-> eq_dep p x q y.
 Proof.
   split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
-- 
cgit v1.2.3