Merge PR #888: Stronger kernel types

3 files changed, 15 insertions, 10 deletions

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c8..6ea8bc7f2c 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
+  let _, univs = Evd.universe_context ctx in
+  let univs =
+    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_polymorphic = Flags.is_universe_polymorphism ();
-	const_entry_universes = snd (Evd.universe_context ctx);
+	const_entry_universes = univs;
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 10d3317f8d..28aeaa725e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+      let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = ty;
-	  const_entry_polymorphic = poly;
-	  const_entry_universes = uctx;
+	  const_entry_universes = univs;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
@@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
   let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-  let body, eff = Future.force entry.const_entry_body in
-  assert(Safe_typing.empty_private_constants = eff);
+  let body, () = Future.force entry.const_entry_body in
   let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
@@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
       let env = Global.env () in
       let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
       let ty = entry.Entries.const_entry_type in
-      let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
-      assert(Safe_typing.empty_private_constants = eff);
+      let (body, cstr), () = Future.force entry.Entries.const_entry_body in
       let sigma = Evd.from_ctx (fst uctx) in
       let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
       Inductiveops.control_only_guard (Global.env ()) body;
diff --git a/vernac/record.ml b/vernac/record.ml
index 63ca227862..a2e443e5f7 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
+                  let univs =
+                    if poly then Polymorphic_const_entry ctx
+                    else Monomorphic_const_entry ctx
+                  in
 		  let entry = {
 		    const_entry_body =
 		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
-		    const_entry_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes = univs;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in