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.

6 files changed, 14 insertions, 48 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index d54efb6328..eedb35acf8 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -217,17 +217,9 @@ let build_id_coercion idf_opt source poly =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = Future.from_val 
-          (mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff);
-        const_entry_secctx = None;
-	const_entry_type = Some typ_f;
-	const_entry_proj = None;
-	const_entry_polymorphic = poly;
-	const_entry_universes = Univ.ContextSet.to_context ctx;
-        const_entry_opaque = false;
-        const_entry_inline_code = true;
-        const_entry_feedback = None;
-      } in
+      (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx)
+	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
+  in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
   let kn = declare_constant idf decl in
   ConstRef kn
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d2111f0fb2..e8d2eda8a7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -655,18 +655,8 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix (_,poly,_ as kind) ctx f def t imps =
-  let ce = {
-    const_entry_body = Future.from_val def;
-    const_entry_secctx = None;
-    const_entry_type = Some t;
-    const_entry_polymorphic = poly;
-    const_entry_universes = ctx;
-    const_entry_proj = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false;
-    const_entry_feedback = None;
-  } in
+let declare_fix (_,poly,_ as kind) ctx f (def,eff) t imps =
+  let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
   declare_definition f kind ce imps (fun _ r -> r)
 
 let _ = Obligations.declare_fix_ref := declare_fix
@@ -855,18 +845,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       let hook l gr = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let ce =
-          { const_entry_body = Future.from_val (Evarutil.nf_evar !evdref body,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = Some ty;
-	    (* FIXME *)
-	    const_entry_proj = None;
-	    const_entry_polymorphic = false;
-	    const_entry_universes = Evd.universe_context !evdref;
-            const_entry_feedback = None;
-        const_entry_opaque = false;
-        const_entry_inline_code = false}
-	in 
+	let univs = Evd.universe_context !evdref in
+	  (*FIXME poly? *)
+	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 2a408e03d1..b406e53029 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -128,7 +128,7 @@ let define internal id c p univs =
     const_entry_type = None;
     const_entry_proj = None;
     const_entry_polymorphic = p;
-    const_entry_universes = Evd.evar_context_universe_context ctx;
+    const_entry_universes = Future.from_val (Evd.evar_context_universe_context ctx);
     const_entry_opaque = false;
     const_entry_inline_code = false;
     const_entry_feedback = None;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index c139f19108..757cdbea9d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -122,7 +122,7 @@ let define id internal ctx c t =
         const_entry_type = t;
 	const_entry_proj = None;
 	const_entry_polymorphic = true;
-	const_entry_universes = Evd.universe_context ctx; (* FIXME *)
+	const_entry_universes = Future.from_val (Evd.universe_context ctx); (* FIXME *)
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d937c400a7..158e452409 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -529,16 +529,9 @@ let subst_body expand prg =
 let declare_definition prg =
   let body, typ = subst_body true prg in
   let ce =
-    { const_entry_body = Future.from_val (body,Declareops.no_seff);
-      const_entry_secctx = None;
-      const_entry_type = Some typ;
-      const_entry_proj = None;
-      const_entry_polymorphic = pi2 prg.prg_kind;
-      const_entry_universes = Univ.ContextSet.to_context prg.prg_ctx;
-      const_entry_opaque = false;
-      const_entry_inline_code = false;
-      const_entry_feedback = None;
-    } in
+    definition_entry ~types:typ ~poly:(pi2 prg.prg_kind) 
+      ~univs:(Univ.ContextSet.to_context prg.prg_ctx) body
+  in
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7411a6377b..b144dfe43c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                     const_entry_secctx = None;
                     const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes = Future.from_val ctx;
 		    const_entry_proj = projinfo;
                     const_entry_opaque = false;
                     const_entry_inline_code = false;