Specific type for section definition entries.

This allows to statically ensure well-formedness properties.

7 files changed, 31 insertions, 5 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 8781c8719..ae28c4b90 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -231,7 +231,15 @@ let cache_variable ((sp,_),o) =
     | SectionLocalDef (de) ->
       let (de, eff) = Global.export_private_constants ~in_section:true de in
       let () = List.iter register_side_effect eff in
-      let univs = Global.push_named_def (id,de) in
+      let body = Future.chain de.const_entry_body (fun (body, ()) -> body) in
+      let se = {
+        secdef_body = body;
+        secdef_secctx = de.const_entry_secctx;
+        secdef_universes = de.const_entry_universes;
+        secdef_feedback = de.const_entry_feedback;
+        secdef_type = de.const_entry_type;
+      } in
+      let univs = Global.push_named_def (id, se) in
       let poly = match de.const_entry_universes with
       | Monomorphic_const_entry _ -> false
       | Polymorphic_const_entry _ -> true
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
diff --git a/library/global.mli b/library/global.mli
index 2a646386e..5d7495657 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t
+val push_named_def   : (Id.t * Entries.section_def_entry) -> Univ.ContextSet.t
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.definition_entry ->