Kernel transparent definition entries have no body universes.

4 files changed, 21 insertions, 17 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca08ba485e..bc389e9fcf 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -57,17 +57,15 @@ type mutual_inductive_entry = {
 }
 
 (** {6 Constants (Definition/Axiom) } *)
-type 'a proof_output = constr Univ.in_universe_context_set * 'a
-type 'a const_entry_body = 'a proof_output Future.computation
 
 type definition_entry = {
-  const_entry_body   : constr Univ.in_universe_context_set;
+  const_entry_body : constr;
   (* List of section variables *)
   const_entry_secctx : Constr.named_context option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
-  const_entry_type        : types option;
-  const_entry_universes   : universes_entry;
+  const_entry_type : types option;
+  const_entry_universes : universes_entry;
   const_entry_inline_code : bool }
 
 type section_def_entry = {
@@ -98,6 +96,9 @@ type primitive_entry = {
   prim_entry_content : CPrimitives.op_or_type;
 }
 
+type 'a proof_output = constr Univ.in_universe_context_set * 'a
+type 'a const_entry_body = 'a proof_output Future.computation
+
 type 'a constant_entry =
   | DefinitionEntry of definition_entry
   | OpaqueEntry of 'a const_entry_body opaque_entry
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7526508c4e..2c434d4edf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff =
   }
   else
   DefinitionEntry {
-    const_entry_body = (p, Univ.ContextSet.empty);
+    const_entry_body = p;
     const_entry_secctx = Some cb.const_hyps;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b3c3dcbf45..5844bd89f8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -194,14 +194,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
-      let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in
+      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       let () = match trust with
       | Pure -> ()
       | SideEffects _ -> assert false
       in
       let env, usubst, univs = match c.const_entry_universes with
-      | Monomorphic_entry univs ->
-        let ctx = Univ.ContextSet.union univs ctx in
+      | Monomorphic_entry ctx ->
         let env = push_context_set ~strict:true ctx env in
         env, Univ.empty_level_subst, Monomorphic ctx
       | Polymorphic_entry (nas, uctx) ->
@@ -210,10 +209,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         let env = push_context ~strict:false uctx env in
         let sbst, auctx = Univ.abstract_universes nas uctx in
         let sbst = Univ.make_instance_subst sbst in
-        let () =
-          if not (Univ.ContextSet.is_empty ctx) then
-            CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
-        in
         env, sbst, Polymorphic auctx
       in
       let j = Typeops.infer env body in
@@ -347,9 +342,8 @@ let translate_recipe env _kn r =
 
 let translate_local_def env _id centry =
   let open Cooking in
-  let body = (centry.secdef_body, Univ.ContextSet.empty) in
   let centry = {
-    const_entry_body = body;
+    const_entry_body = centry.secdef_body;
     const_entry_secctx = centry.secdef_secctx;
     const_entry_feedback = centry.secdef_feedback;
     const_entry_type = centry.secdef_type;
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 74196bb875..aa94ab5a25 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -173,12 +173,21 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
 let cast_proof_entry e =
   let open Proof_global in
   let (body, ctx), () = Future.force e.proof_entry_body in
+  let univs =
+    if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
+    else match e.proof_entry_universes with
+      | Monomorphic_entry ctx' ->
+        (* This can actually happen, try compiling EqdepFacts for instance *)
+        Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
+      | Polymorphic_entry _ ->
+        anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
+  in
   {
-    const_entry_body = (body, ctx);
+    const_entry_body = body;
     const_entry_secctx = e.proof_entry_secctx;
     const_entry_feedback = e.proof_entry_feedback;
     const_entry_type = e.proof_entry_type;
-    const_entry_universes = e.proof_entry_universes;
+    const_entry_universes = univs;
     const_entry_inline_code = e.proof_entry_inline_code;
   }