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

25 files changed, 88 insertions, 94 deletions

diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
new file mode 100644
index 0000000000..6dc44aa627
--- /dev/null
+++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then
+
+    equations_CI_REF=proofs+declare_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 60717c6eec..352b21a15a 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1170,7 +1170,7 @@ let get_funs_constant mp =
     in
     l_const
 
-let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
+let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list =
   let exception Found_type of int in
   let env = Global.env () in
   let funs = List.map fst fas in
@@ -1244,7 +1244,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
     | Some equation ->
       Declareops.is_opaque (Global.lookup_constant equation)
   in
-  let const = {const with Proof_global.proof_entry_opaque = opacity } in
+  let const = {const with Declare.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
   if List.is_empty other_princ_types
   then
@@ -1255,8 +1255,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
       let sorts = Array.of_list sorts in
       List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let open Proof_global in
-    let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
+    let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in
     let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
     let other_result =
@@ -1299,10 +1298,10 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
            let princ_body =
              Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
            in
-           {const with
-              proof_entry_body =
-                (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
-              proof_entry_type = Some scheme_type
+           { const with
+             Declare.proof_entry_body =
+               (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
+             proof_entry_type = Some scheme_type
            }
       )
       other_fun_princ_types
@@ -1358,7 +1357,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
              Array.of_list
                (List.map
                   (fun entry ->
-                     (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
+                     (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))),
+                      EConstr.of_constr (Option.get entry.Declare.proof_entry_type ))
                   )
                   (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
                )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7719705138..ba37b9b461 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -115,7 +115,7 @@ open DeclareDef
 let definition_message = Declare.definition_message
 
 let save name const ?hook uctx scope kind =
-  let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
+  let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 16beaaa3c7..34fb10bb67 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -44,7 +44,7 @@ val make_eq : unit -> EConstr.constr
 
 val save
   :  Id.t
-  -> Evd.side_effects Proof_global.proof_entry
+  -> Evd.side_effects Declare.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> DeclareDef.locality
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 0ce726db25..756fef0511 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -6,9 +6,7 @@ Proof
 Logic
 Goal_select
 Proof_bullet
-Proof_global
 Refiner
 Tacmach
-Pfedit
 Clenv
 Clenvtac
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 09d7e0278a..edeb27ab88 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu =
 | _ -> assert false
 
 let shrink_entry sign const =
-  let open Proof_global in
+  let open Declare in
   let typ = match const.proof_entry_type with
   | None -> assert false
   | Some t -> t
@@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
+  let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in
   let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
@@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
-  let inst = match const.Proof_global.proof_entry_universes with
+  let inst = match const.Declare.proof_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
     (* We mimic what the kernel does, that is ensuring that no additional
        constraints appear in the body of polymorphic constants. Ideally this
        should be enforced statically. *)
-    let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in
+    let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in
     let () = assert (Univ.ContextSet.is_empty body_uctx) in
     EInstance.make (Univ.UContext.instance ctx)
   in
   let lem = mkConstU (cst, inst) in
   let evd = Evd.set_universe_context evd ectx in
   let effs = Evd.concat_side_effects eff
-    Proof_global.(snd (Future.force const.proof_entry_body)) in
+      (snd (Future.force const.Declare.proof_entry_body)) in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index e278729f89..96ddbea7b2 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P
    save path *)
 val shrink_entry
   :  ('a, 'b) Context.Named.Declaration.pt list
-  -> 'c Proof_global.proof_entry
-  -> 'c Proof_global.proof_entry * Constr.t list
+  -> 'c Declare.proof_entry
+  -> 'c Declare.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c280760e84..694bd6d1cd 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -55,8 +55,20 @@ type constant_obj = {
   cst_locl : import_status;
 }
 
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 type 'a constant_entry =
-  | DefinitionEntry of 'a Proof_global.proof_entry
+  | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
@@ -174,7 +186,6 @@ let record_aux env s_ty s_bo =
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
-  let open Proof_global in
   { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     proof_entry_secctx = None;
     proof_entry_type = types;
@@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     proof_entry_inline_code = inline}
 
 let cast_proof_entry e =
-  let open Proof_global in
   let (body, ctx), () = Future.force e.proof_entry_body in
   let univs =
     if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
@@ -205,7 +215,6 @@ let cast_proof_entry e =
   }
 
 let cast_opaque_proof_entry e =
-  let open Proof_global in
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -249,7 +258,6 @@ let is_unsafe_typing_flags () =
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 let define_constant ~side_effect ~name cd =
-  let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let in_section = Lib.sections_are_opened () in
   let export, decl, unsafe = match cd with
@@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
 
 (** Declaration of section variables and local definitions *)
 type variable_declaration =
-  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 (* This object is only for things which iterate over objects to find
@@ -321,7 +329,6 @@ let declare_variable ~name ~kind d =
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
-      let open Proof_global in
       let (body, eff) = Future.force de.proof_entry_body in
       let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in
       let eff = get_roles export eff in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4ae9f6c7ae..4cb876cecb 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -19,14 +19,27 @@ open Entries
    reset works properly --- and will fill some global tables such as
    [Nametab] and [Impargs]. *)
 
+(** Proof entries *)
+type 'a proof_entry = {
+  proof_entry_body   : 'a Entries.const_entry_body;
+  (* List of section variables *)
+  proof_entry_secctx : Constr.named_context option;
+  (* State id on which the completion of type checking is reported *)
+  proof_entry_feedback : Stateid.t option;
+  proof_entry_type        : Constr.types option;
+  proof_entry_universes   : Entries.universes_entry;
+  proof_entry_opaque      : bool;
+  proof_entry_inline_code : bool;
+}
+
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type variable_declaration =
-  | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
+  | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind }
 
 type 'a constant_entry =
-  | DefinitionEntry of 'a Proof_global.proof_entry
+  | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
@@ -43,7 +56,7 @@ val declare_variable
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
-  ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
+  ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e2ef05461b..1f973ace6f 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -125,7 +125,7 @@ let define internal role id c poly univs =
   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 = {
-    Proof_global.proof_entry_body =
+    Declare.proof_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
                        Evd.empty_side_effects);
     proof_entry_secctx = None;
diff --git a/proofs/pfedit.ml b/tactics/pfedit.ml
index 99a254652c..5be7b4fa28 100644
--- a/proofs/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -124,7 +124,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac =
     let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
-      let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in
+      let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in
       entry, status, univs
     | _ ->
       CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
@@ -136,7 +136,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
-  let body, eff = Future.force ce.Proof_global.proof_entry_body in
+  let body, eff = Future.force ce.Declare.proof_entry_body in
   let (cb, ctx) =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
     else body
diff --git a/proofs/pfedit.mli b/tactics/pfedit.mli
index 0626e40047..30514191fa 100644
--- a/proofs/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -64,7 +64,7 @@ val build_constant_by_tactic
   -> poly:bool
   -> EConstr.types
   -> unit Proofview.tactic
-  -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
+  -> Evd.side_effects Declare.proof_entry * bool * UState.t
 
 val build_by_tactic
   :  ?side_eff:bool
diff --git a/proofs/proof_global.ml b/tactics/proof_global.ml
index 851a3d1135..a2929e45cd 100644
--- a/proofs/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -24,21 +24,9 @@ module NamedDecl = Context.Named.Declaration
 
 (*** Proof Global Environment ***)
 
-type 'a proof_entry = {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
-  (* State id on which the completion of type checking is reported *)
-  proof_entry_feedback : Stateid.t option;
-  proof_entry_type        : Constr.types option;
-  proof_entry_universes   : Entries.universes_entry;
-  proof_entry_opaque      : bool;
-  proof_entry_inline_code : bool;
-}
-
 type proof_object =
   { name : Names.Id.t
-  ; entries : Evd.side_effects proof_entry list
+  ; entries : Evd.side_effects Declare.proof_entry list
   ; poly : bool
   ; universes: UState.t
   ; udecl : UState.universe_decl
@@ -223,7 +211,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
           let ctx = UState.restrict universes used_univs in
           let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
-      in 
+      in
        fun t p -> Future.split2 (Future.chain p (make_body t))
     else
       fun t p ->
@@ -250,6 +238,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     let t = EConstr.Unsafe.to_constr t in
     let univstyp, body = make_body t p in
     let univs, typ = Future.force univstyp in
+    let open Declare in
     {
       proof_entry_body = body;
       proof_entry_secctx = section_vars;
diff --git a/proofs/proof_global.mli b/tactics/proof_global.mli
index 54d5c2087a..d15e23c2cc 100644
--- a/proofs/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -27,29 +27,11 @@ val get_initial_euctx : t -> UState.t
 
 val compact_the_proof : t -> t
 
-(** When a proof is closed, it is reified into a [proof_object], where
-    [id] is the name of the proof, [entries] the list of the proof terms
-    (in a form suitable for definitions). Together with the [terminator]
-    function which takes a [proof_object] together with a [proof_end]
-    (i.e. an proof ending command) and registers the appropriate
-    values. *)
-type 'a proof_entry = {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
-  (* State id on which the completion of type checking is reported *)
-  proof_entry_feedback : Stateid.t option;
-  proof_entry_type        : Constr.types option;
-  proof_entry_universes   : Entries.universes_entry;
-  proof_entry_opaque      : bool;
-  proof_entry_inline_code : bool;
-}
-
 (** When a proof is closed, it is reified into a [proof_object] *)
 type proof_object =
   { name : Names.Id.t
   (** name of the proof *)
-  ; entries : Evd.side_effects proof_entry list
+  ; entries : Evd.side_effects Declare.proof_entry list
   (** list of the proof terms (in a form suitable for definitions). *)
   ; poly : bool
   (** polymorphic status *)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 6dd749aa0d..c5c7969a09 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,4 +1,6 @@
 Declare
+Proof_global
+Pfedit
 Dnet
 Dn
 Btermdn
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);