Enforce that transparent entries are forced beforehand.

3 files changed, 8 insertions, 12 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 1a25337512..3f33df3f74 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -61,7 +61,7 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
 type 'a definition_entry = {
-  const_entry_body   : 'a const_entry_body;
+  const_entry_body   : 'a;
   (* List of section variables *)
   const_entry_secctx : Constr.named_context option;
   (* State id on which the completion of type checking is reported *)
@@ -89,8 +89,8 @@ type primitive_entry = {
 }
 
 type 'a constant_entry =
-  | DefinitionEntry of 'a definition_entry
-  | OpaqueEntry of 'a definition_entry
+  | DefinitionEntry of constr Univ.in_universe_context_set definition_entry
+  | OpaqueEntry of 'a const_entry_body definition_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c99edccda7..ab58321ac7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff =
     const_entry_inline_code = cb.const_inline_code }
   else
   DefinitionEntry {
-    const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
+    const_entry_body = (p, Univ.ContextSet.empty);
     const_entry_secctx = None;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e28849c953..3b689953c8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -196,13 +196,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
       let { const_entry_type = typ; _ } = c in
-      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
-      (* Opaque constants must be provided with a non-empty const_entry_type,
-         and thus should have been treated above. *)
-      let body, ctx = match trust with
-      | Pure ->
-        let (body, ctx), () = Future.join body in
-        body, ctx
+      let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in
+      let () = match trust with
+      | Pure -> ()
       | SideEffects _ -> assert false
       in
       let env, usubst, univs = match c.const_entry_universes with
@@ -366,7 +362,7 @@ let translate_recipe env _kn r =
 
 let translate_local_def env _id centry =
   let open Cooking in
-  let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in
+  let body = (centry.secdef_body, Univ.ContextSet.empty) in
   let centry = {
     const_entry_body = body;
     const_entry_secctx = centry.secdef_secctx;