Specific type for section definition entries.

This allows to statically ensure well-formedness properties.

5 files changed, 21 insertions, 3 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404..35a158682 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,14 @@ type 'a definition_entry = {
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
+type section_def_entry = {
+  secdef_body : constr Univ.in_universe_context_set Future.computation;
+  secdef_secctx : Context.Named.t option;
+  secdef_feedback : Stateid.t option;
+  secdef_type : types option;
+  secdef_universes : constant_universes_entry;
+}
+
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fa984515a..4fbe02cf5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -384,7 +384,7 @@ let safe_push_named d env =
 let push_named_def (id,de) senv =
   let open Entries in
   let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let poly = match de.Entries.const_entry_universes with
+  let poly = match de.Entries.secdef_universes with
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fbc398a2a..faa758d07 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer
+  Id.t * Entries.section_def_entry -> Univ.ContextSet.t safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 761eab511..c2c65d6d4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -607,6 +607,16 @@ let translate_recipe env kn r =
 
 let translate_local_def env id centry =
   let open Cooking in
+  let body = Future.chain centry.secdef_body (fun body -> body, ()) in
+  let centry = {
+    const_entry_body = body;
+    const_entry_secctx = centry.secdef_secctx;
+    const_entry_feedback = centry.secdef_feedback;
+    const_entry_type = centry.secdef_type;
+    const_entry_universes = centry.secdef_universes;
+    const_entry_opaque = false;
+    const_entry_inline_code = false;
+  } in
   let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c771452a1..4b893b056 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,7 +18,7 @@ type _ trust =
 | Pure : unit trust
 | SideEffects : structure_body -> side_effects trust
 
-val translate_local_def : env -> Id.t -> unit definition_entry ->
+val translate_local_def : env -> Id.t -> section_def_entry ->
   constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types