From 5a532f2e00d0e3dca8d7079f067c79f2bb1b6b14 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Jun 2019 13:36:39 +0200
Subject: Kernel transparent definition entries have no body universes.

---
 kernel/entries.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel/entries.ml')

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
-- 
cgit v1.2.3