From 57bee17f928fc67a599d2116edb42a59eeb21477 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Oct 2013 18:30:54 +0200
Subject: Rework handling of universes on top of the STM, allowing for delayed
 computation in case of non-polymorphic proofs. Also fix plugins after
 forgotten merge conflicts. Still does not compile everything.

---
 plugins/funind/functional_principles_types.ml | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2adc825056..88693c1967 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -340,19 +340,7 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce =
-          { const_entry_body =
-              Future.from_val (value,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = None;	
-	    const_entry_polymorphic = false;
-	    const_entry_universes = Univ.UContext.empty (*FIXME*);
-	    const_entry_proj = None;
-	    const_entry_opaque = false;
-            const_entry_feedback = None;
-	    const_entry_inline_code = false
-	  }
-	in
+	let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
 	ignore(
 	  Declare.declare_constant
 	    name
-- 
cgit v1.2.3