[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`.

10 files changed, 24 insertions, 27 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 57de719cb4..9745358ba2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
   in
   if program_mode then
     let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in
+    let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
     assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
     assert(Univ.ContextSet.is_empty ctx);
     Obligations.check_evars env evd;
     let c = EConstr.of_constr c in
-    let typ = match ce.Proof_global.proof_entry_type with
+    let typ = match ce.Declare.proof_entry_type with
       | Some t -> EConstr.of_constr t
       | None -> Retyping.get_type_of env evd c
     in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index db0c102e14..01505d0733 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -41,5 +41,5 @@ val interp_definition
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Evd.side_effects Proof_global.proof_entry *
+  -> Evd.side_effects Declare.proof_entry *
      Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 5e4f2dcd34..1926faaf0e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -44,7 +44,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
-  let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
+  let fix_exn = Future.fix_exn_of ce.proof_entry_body in
   let gr = match scope with
   | Discharge ->
       let () =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 606cfade46..54a0c9a7e8 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -45,7 +45,7 @@ val declare_definition
   -> kind:Decls.definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
-  -> Evd.side_effects Proof_global.proof_entry
+  -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
   -> GlobRef.t
 
@@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool ->
   ?opaque:bool -> ?inline:bool -> poly:bool ->
   Evd.evar_map -> UState.universe_decl ->
   types:EConstr.t option -> body:EConstr.t ->
-  Evd.evar_map * Evd.side_effects Proof_global.proof_entry
+  Evd.evar_map * Evd.side_effects Declare.proof_entry
 
 val prepare_parameter : allow_evars:bool ->
   poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
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
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 2a8fa734b3..7d8a112cc6 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -76,7 +76,7 @@ type obligation_qed_info =
   }
 
 val obligation_terminator
-  : Evd.side_effects Proof_global.proof_entry list
+  : Evd.side_effects Declare.proof_entry list
   -> UState.t
   -> obligation_qed_info -> unit
 (** [obligation_terminator] part 2 of saving an obligation *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index cf87646905..18955c2ba3 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -101,7 +101,6 @@ let () =
 let define ~poly name sigma c t =
   let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
   let univs = Evd.univ_entry ~poly sigma in
-  let open Proof_global in
   let kn = f ~name
     (DefinitionEntry
       { proof_entry_body = c;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7809425a10..42d1a1f3fc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function
   | possible_indexes ->
     (* Try all combinations... not optimal *)
     let env = Global.env() in
-    let open Proof_global in
     { const with
-      proof_entry_body =
-        Future.chain const.proof_entry_body
+      Declare.proof_entry_body =
+        Future.chain const.Declare.proof_entry_body
           (fun ((body, ctx), eff) ->
              match Constr.kind body with
              | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info =
     let name = match idopt with
       | None -> name
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
-    let fix_exn = Future.fix_exn_of const.proof_entry_body in
+    let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
-      let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
+      let should_suggest = const.Declare.proof_entry_opaque &&
+                           Option.is_empty const.Declare.proof_entry_secctx in
       let open DeclareDef in
       let r = match scope with
         | Discharge ->
@@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries =
   in
   (* The opacity of [f_def] is adjusted to be [false], as it
      must. Then [f] is declared in the global environment. *)
-  let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
+  let f_def = { f_def with Declare.proof_entry_opaque = false } in
   let f_kind = Decls.(IsDefinition Definition) in
   let f_def = Declare.DefinitionEntry f_def in
   let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
@@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries =
   let substf c = Vars.replace_vars [f,f_kn_term] c in
   (* Extracts the type of the proof of [suchthat]. *)
   let lemma_pretype =
-    match Proof_global.(lemma_def.proof_entry_type) with
+    match lemma_def.Declare.proof_entry_type with
     | Some t -> t
     | None -> assert false (* Proof_global always sets type here. *)
   in
   (* The references of [f] are subsituted appropriately. *)
   let lemma_type = substf lemma_pretype in
   (* The same is done in the body of the proof. *)
-  let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
-  let lemma_def = let open Proof_global in
+  let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+  let lemma_def =
     { lemma_def with
-      proof_entry_body = lemma_body;
+      Declare.proof_entry_body = lemma_body;
       proof_entry_type = Some lemma_type }
   in
   let lemma_def = Declare.DefinitionEntry lemma_def in
@@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info =
   let { Info.hook; scope; impargs; other_thms } = info in
   if List.length entries <> 1 then
     user_err Pp.(str "Admitted does not support multiple statements");
-  let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+  let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
   let poly = match proof_entry_universes with
     | Entries.Monomorphic_entry _ -> false
     | Entries.Polymorphic_entry (_, _) -> true in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 37fe0df0ee..5d153fa8be 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx =
       Pfedit.build_constant_by_tactic
         ~name ~poly ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
-    let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
+    let (body, eff) = Future.force entry.Declare.proof_entry_body in
     let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
     let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
     Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
-    Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx')
+    Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx')
   with
   | Refiner.FailError (_, s) as exn ->
     let _ = CErrors.push exn in
diff --git a/vernac/record.ml b/vernac/record.ml
index 86745212e7..1bb8ddf5dc 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -340,7 +340,6 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-                  let open Proof_global in
 		  let entry = {
                     proof_entry_body =
                       Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);