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.

---
 pretyping/tacred.ml         | 2 +-
 theories/Logic/EqdepFacts.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67aef0cfcd..0088563fab 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1071,7 +1071,7 @@ let is_projection env = function
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
   if is_projection env name then
-    error ("Cannot unfold primitie projection " ^ string_of_evaluable_ref env name)
+    error ("Cannot unfold primitive projection " ^ string_of_evaluable_ref env name)
   else
   let unfo nowhere_except_in locs =
     let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
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