From d104b50b9c9a589d9fd8e44bdf56794c8aea4e53 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 14:15:08 +0200
Subject: Safer entry point of primitive projections in the kernel, now it does
 recognize a projection constant only of the form  λ params (r : I params),
 match r with BuildR args => args_i end, without any other user input and
 relies on it being typable (no more primitive projections escaping this).

---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 89939b864d..7c44f1500d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -327,7 +327,7 @@ let close_proof ?feedback_id ~now fpl =
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
 	  const_entry_polymorphic = poly;
-	  const_entry_proj = None})
+	  const_entry_proj = false})
       fpl initial_goals in
   { id = pid; entries = entries; persistence = strength; universes = univsubst },
   Ephemeron.get terminator
-- 
cgit v1.2.3