Merge PR #10884: Last stop before CEP 40

Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares

1 files changed, 11 insertions, 2 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 54393dce00..3f824a94bf 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,8 +124,17 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = Declare.definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
+  let entry = {
+    Declare.proof_entry_body =
+      Future.from_val ((c,Univ.ContextSet.empty), ());
+    proof_entry_secctx = None;
+    proof_entry_type = None;
+    proof_entry_universes = univs;
+    proof_entry_opaque = false;
+    proof_entry_inline_code = false;
+    proof_entry_feedback = None;
+  } in
+  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id