Specific type for section definition entries.

This allows to statically ensure well-formedness properties.

1 files changed, 10 insertions, 0 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 761eab511a..c2c65d6d48 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