From 31e4222d35b614efa94a1d68b5d6491ea9e46bfa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 24 Sep 2014 11:11:28 +0200
Subject: Return a Prop not an arbitrary Type, and correct a typo.

---
 theories/Logic/EqdepFacts.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 58b6d076c5..afd0ecf046 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -376,7 +376,7 @@ Proof.
                          (eq_sym (UIP (eq_refl x) (eq_refl x)))).
   - destruct z. unfold e. destruct (UIP _ _). reflexivity.
   - change
-      (match eq_refl x as y' in _ = x' return y' = y' -> Type with
+      (match eq_refl x as y' in _ = x' return y' = y' -> Prop with
        | eq_refl => fun z => z = (eq_refl (eq_refl x))
        end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
                      (eq_sym (UIP (eq_refl x) (eq_refl x))))).
-- 
cgit v1.2.3