Merge PR #10674: [declare] Move proof_entry type to declare, put interactive proof data on top of declare.

Reviewed-by: ppedrot

25 files changed, 113 insertions, 162 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..92b7f2accf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
-let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
   (*   let time1 = System.get_time ()  in *)
@@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    name, entry, hook
+    entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -282,7 +282,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort Sorts.InProp;
       register_with_sort Sorts.InSet
   in
-  let id,entry,hook =
+  let entry, hook =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -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
@@ -1219,9 +1219,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
         s::l_schemes -> s,l_schemes
       | _ -> CErrors.anomaly (Pp.str "")
   in
-  let _,const,_ =
+  let opaque =
+    let finfos =
+      match find_Function_infos (fst first_fun) with
+      | None -> raise Not_found
+      | Some finfos -> finfos
+    in
+    let open Proof_global in
+    match finfos.equation_lemma with
+    | None -> Transparent (* non recursive definition *)
+    | Some equation ->
+      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent
+  in
+  let entry, _hook =
     try
-      build_functional_principle evd false
+      build_functional_principle ~opaque evd false
         first_type
         (Array.of_list sorts)
         this_block_funs
@@ -1233,30 +1245,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
 
   in
   incr i;
-  let opacity =
-    let finfos =
-      match find_Function_infos (fst first_fun) with
-      | None -> raise Not_found
-      | Some finfos -> finfos
-    in
-    match finfos.equation_lemma with
-    | None -> false (* non recursive definition *)
-    | Some equation ->
-      Declareops.is_opaque (Global.lookup_constant equation)
-  in
-  let const = {const with Proof_global.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
   if List.is_empty other_princ_types
-  then
-    [const]
+  then [entry]
   else
     let other_fun_princ_types =
       let funs = Array.map Constr.mkConstU this_block_funs in
       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.(entry.proof_entry_body, entry.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 =
@@ -1283,7 +1281,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
              (* If we reach this point, the two principle are not mutually recursive
                 We fall back to the previous method
                 *)
-             let _,const,_ =
+             let entry, _hook =
                build_functional_principle
                  evd
                  false
@@ -1294,20 +1292,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
                  (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
                  (fun _ _ -> ())
              in
-             const
+             entry
          with Found_type i ->
            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
-           }
+           Declare.definition_entry ~types:scheme_type princ_body
       )
       other_fun_princ_types
     in
-    const::other_result
+    entry::other_result
 
 (* [derive_correctness funs graphs] create correctness and completeness
    lemmas for each function in [funs] w.r.t. [graphs]
@@ -1358,7 +1352,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 16c0521eda..6d91c2a348 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -117,7 +117,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 c23ee4a76e..3a02e5451a 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..54393dce00 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,17 +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 = {
-    Proof_global.proof_entry_body =
-      Future.from_val ((c,Univ.ContextSet.empty),
-                       Evd.empty_side_effects);
-    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.definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
   let () = match internal with
     | InternalTacticRequest -> ()
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..e3cffa8523 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
       if get_shrink_obligations () && not poly then shrink_body body ty
       else ([], body, ty, [||])
     in
-    let body =
-      ((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
-      ; proof_entry_secctx = None
-      ; proof_entry_type = ty
-      ; proof_entry_universes = uctx
-      ; proof_entry_opaque = opaque
-      ; proof_entry_inline_code = false
-      ; proof_entry_feedback = None }
-    in
+    let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant ~name:obl.obl_name
@@ -495,12 +485,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 +503,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..a6c577a878 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -98,20 +98,11 @@ let () =
 
 (* Util *)
 
-let define ~poly name sigma c t =
+let define ~poly name sigma c types =
   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;
-        proof_entry_secctx = None;
-        proof_entry_type = t;
-        proof_entry_universes = univs;
-        proof_entry_opaque = false;
-        proof_entry_inline_code = false;
-        proof_entry_feedback = None;
-      }) in
+  let entry = Declare.definition_entry ~univs ?types c in
+  let kn = f ~name (DefinitionEntry entry) in
   definition_message name;
   kn
 
@@ -412,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
-    let cst = define ~poly fi sigma proof_output (Some decltype) in
+    let cst = define ~poly fi sigma decl (Some decltype) in
     GlobRef.ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -534,7 +524,6 @@ let do_combined_scheme name schemes =
       schemes
   in
   let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
   (* It is possible for the constants to have different universe
      polymorphism from each other, however that is only when the user
      manually defined at least one of them (as Scheme would pick the
@@ -542,7 +531,7 @@ let do_combined_scheme name schemes =
      some other polymorphism they can also manually define the
      combined scheme. *)
   let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
-  ignore (define ~poly name.v sigma proof_output (Some typ));
+  ignore (define ~poly name.v sigma body (Some typ));
   fixpoint_message None [name.v]
 
 (**********************************************************************)
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..11237f3873 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -340,16 +340,7 @@ 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);
-                    proof_entry_secctx = None;
-                    proof_entry_type = Some projtyp;
-                    proof_entry_universes = ctx;
-                    proof_entry_opaque = false;
-                    proof_entry_inline_code = false;
-                    proof_entry_feedback = None } in
+                  let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
                   let kind = Decls.IsDefinition kind in
                   let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
 		  let constr_fip =