Enforce that transparent entries are forced beforehand.

4 files changed, 22 insertions, 14 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;
diff --git a/tactics/declare.ml b/tactics/declare.ml
index b35d4a5d66..2178a7c54c 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -162,6 +162,18 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
 
 let cast_proof_entry e =
   let open Proof_global in
+  let (body, ctx), () = Future.force e.proof_entry_body in
+  {
+    const_entry_body = (body, ctx);
+    const_entry_secctx = e.proof_entry_secctx;
+    const_entry_feedback = e.proof_entry_feedback;
+    const_entry_type = e.proof_entry_type;
+    const_entry_universes = e.proof_entry_universes;
+    const_entry_inline_code = e.proof_entry_inline_code;
+  }
+
+let cast_opaque_proof_entry e =
+  let open Proof_global in
   {
     const_entry_body = e.proof_entry_body;
     const_entry_secctx = e.proof_entry_secctx;
@@ -198,7 +210,7 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = match de.proof_entry_opaque with
-      | true -> Entries.OpaqueEntry (cast_proof_entry de)
+      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de)
       | false -> Entries.DefinitionEntry (cast_proof_entry de)
       in
       export, ConstantEntry (PureEntry, cd)
@@ -207,7 +219,7 @@ let define_constant ~side_effect ?(export_seff=false) id cd =
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
-      let de = cast_proof_entry de in
+      let de = cast_opaque_proof_entry de in
       [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
     | ParameterEntry e ->
       [], ConstantEntry (PureEntry, Entries.ParameterEntry e)