From 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 30 Aug 2014 18:48:11 +0200
Subject: Simplify even further the declaration of primitive projections, now
 done entirely using declare_mind, which declares the associated constants for
 primitive records. This avoids a hack related to elimination schemes and
 ensures that the forward references to constants in the mutual inductive
 entry are properly declared just after the inductive. This also clarifies
 (and simplifies) the code of term_typing for constants which does not have to
 deal with building or checking projections anymore. Also fix printing of
 universes showing the de Bruijn encoding in a few places.

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

(limited to 'proofs')

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