Merge PR #10438: Kernel transparent definition entries have no body universes.

Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 6 insertions, 5 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