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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3