[declare] Move proof_entry type to declare, put interactive proof data on top of declare.

This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.

This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.

This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.

A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.

Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.

1 files changed, 4 insertions, 5 deletions

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c5cbb095ca..9c8213ad8a 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -153,7 +153,7 @@ let declare_obligation prg obl body ty uctx =
       ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
     in
     let ce =
-      Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
+      { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
       ; proof_entry_secctx = None
       ; proof_entry_type = ty
       ; proof_entry_universes = uctx
@@ -495,12 +495,11 @@ type obligation_qed_info =
   }
 
 let obligation_terminator entries uctx { name; num; auto } =
-  let open Proof_global in
   match entries with
   | [entry] ->
     let env = Global.env () in
-    let ty = entry.proof_entry_type in
-    let body, eff = Future.force entry.proof_entry_body in
+    let ty = entry.Declare.proof_entry_type in
+    let body, eff = Future.force entry.Declare.proof_entry_body in
     let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
@@ -514,7 +513,7 @@ let obligation_terminator entries uctx { name; num; auto } =
     let obls, rem = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
-      match obl.obl_status, entry.proof_entry_opaque with
+      match obl.obl_status, entry.Declare.proof_entry_opaque with
       | (_, Evar_kinds.Expand), true -> err_not_transp ()
       | (true, _), true -> err_not_transp ()
       | (false, _), true -> Evar_kinds.Define true