[declare] Make `proof_entry` a private type.

Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.

This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.

So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.

To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.

1 files changed, 1 insertions, 10 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 3f824a94bf..ac98b5f116 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,16 +124,7 @@ 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.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 entry = Declare.pure_definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
   let () = match internal with
     | InternalTacticRequest -> ()