[proof] Merge `Proof_global` into `Declare`

We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]

Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.

16 files changed, 91 insertions, 92 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 2b661888e4..215d5d97a0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -699,7 +699,7 @@ let make_bl_scheme mode mind =
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
-  let (ans, _, _, ctx) = Proof_global.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
+  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -829,7 +829,7 @@ let make_lb_scheme mode mind =
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
-  let (ans, _, _, ctx) = Proof_global.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
+  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -1006,7 +1006,7 @@ let make_eq_decidability mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
-  let (ans, _, _, ctx) = Proof_global.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
+  let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
       ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
       (compute_dec_tact ind lnamesparrec nparrec)
   in
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 247f80181a..058fa691ee 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,7 +14,6 @@ open Glob_term
 open Constrexpr
 open Vernacexpr
 open Hints
-open Proof_global
 
 open Pcoq
 open Pcoq.Prim
@@ -65,12 +64,12 @@ GRAMMAR EXTEND Gram
       | IDENT "Existential"; n = natural; c = constr_body ->
           { VernacSolveExistential (n,c) }
       | IDENT "Admitted" -> { VernacEndProof Admitted }
-      | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) }
+      | IDENT "Qed" -> { VernacEndProof (Proved (Declare.Opaque,None)) }
       | IDENT "Save"; id = identref ->
-          { VernacEndProof (Proved (Opaque, Some id)) }
-      | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) }
+          { VernacEndProof (Proved (Declare.Opaque, Some id)) }
+      | IDENT "Defined" -> { VernacEndProof (Proved (Declare.Transparent,None)) }
       |	IDENT "Defined"; id=identref ->
-          { VernacEndProof (Proved (Transparent,Some id)) }
+          { VernacEndProof (Proved (Declare.Transparent,Some id)) }
       | IDENT "Restart" -> { VernacRestart }
       | IDENT "Undo" -> { VernacUndo 1 }
       | IDENT "Undo"; n = natural -> { VernacUndo n }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b0f33b7558..f5a7307028 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -62,14 +62,14 @@ end
 
 (* Proofs with a save constant function *)
 type t =
-  { proof : Proof_global.t
+  { proof : Declare.t
   ; info : Info.t
   }
 
 let pf_map f pf = { pf with proof = f pf.proof }
 let pf_fold f pf = f pf.proof
 
-let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
+let set_endline_tactic t = pf_map (Declare.set_endline_tactic t)
 
 (* To be removed *)
 module Internal = struct
@@ -81,7 +81,7 @@ module Internal = struct
 end
 
 let by tac pf =
-  let proof, res = Proof_global.by tac pf.proof in
+  let proof, res = Declare.by tac pf.proof in
   { pf with proof }, res
 
 (************************************************************************)
@@ -113,7 +113,7 @@ let start_lemma ~name ~poly
      "opaque", this is a hack tho, see #10446 *)
   let sign = initialize_named_context_for_proof () in
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in
+  let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in
   let info = add_first_thm ~info ~name ~typ:c ~impargs in
   { proof; info }
 
@@ -123,7 +123,7 @@ let start_lemma ~name ~poly
 let start_dependent_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
     ?(info=Info.make ()) telescope =
-  let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly telescope in
+  let proof = Declare.start_dependent_proof ~name ~udecl ~poly telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
@@ -173,7 +173,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     (* start_lemma has the responsibility to add (name, impargs, typ)
        to thms, once Info.t is more refined this won't be necessary *)
     let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
-    pf_map (Proof_global.map_proof (fun p ->
+    pf_map (Declare.map_proof (fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
 (************************************************************************)
@@ -275,7 +275,7 @@ let get_keep_admitted_vars =
 
 let compute_proof_using_for_admitted proof typ pproofs =
   if not (get_keep_admitted_vars ()) then None
-  else match Proof_global.get_used_variables proof, pproofs with
+  else match Declare.get_used_variables proof, pproofs with
     | Some _ as x, _ -> x
     | None, pproof :: _ ->
       let env = Global.env () in
@@ -291,17 +291,17 @@ let finish_admitted ~info ~uctx pe =
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
-  let udecl = Proof_global.get_universe_decl lemma.proof in
-  let Proof.{ poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let udecl = Declare.get_universe_decl lemma.proof in
+  let Proof.{ poly; entry } = Proof.data (Declare.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
     | [typ] -> snd typ
     | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
   in
   let typ = EConstr.Unsafe.to_constr typ in
-  let proof = Proof_global.get_proof lemma.proof in
+  let proof = Declare.get_proof lemma.proof in
   let pproofs = Proof.partial_proof proof in
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
-  let uctx = Proof_global.get_initial_euctx lemma.proof in
+  let uctx = Declare.get_initial_euctx lemma.proof in
   let univs = UState.check_univ_decl ~poly uctx udecl in
   finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None)
 
@@ -310,7 +310,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
 (************************************************************************)
 
 let finish_proved po info =
-  let open Proof_global in
+  let open Declare in
   match po with
   | { entries=[const]; uctx } ->
     let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
@@ -343,7 +343,7 @@ let finish_derived ~f ~name ~entries =
   let lemma_pretype typ =
     match typ with
     | Some t -> Some (substf t)
-    | None -> assert false (* Proof_global always sets type here. *)
+    | None -> assert false (* Declare always sets type here. *)
   in
   (* The references of [f] are subsituted appropriately. *)
   let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in
@@ -368,12 +368,12 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
         let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
         sigma, cst) sigma0
-      types proof_obj.Proof_global.entries
+      types proof_obj.Declare.entries
   in
   hook recobls sigma
 
 let finalize_proof proof_obj proof_info =
-  let open Proof_global in
+  let open Declare in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
@@ -403,7 +403,7 @@ let process_idopt_for_save ~idopt info =
 
 let save_lemma_proved ~lemma ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in
+  let proof_obj = Declare.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in
   let proof_info = process_idopt_for_save ~idopt lemma.info in
   finalize_proof proof_obj proof_info
 
@@ -411,7 +411,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt =
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
 let save_lemma_admitted_delayed ~proof ~info =
-  let open Proof_global in
+  let open Declare in
   let { entries; uctx } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
@@ -430,7 +430,7 @@ let save_lemma_proved_delayed ~proof ~info ~idopt =
   (* vio2vo calls this but with invalid info, we have to workaround
      that to add the name to the info structure *)
   if CList.is_empty info.Info.thms then
-    let info = add_first_thm ~info ~name:proof.Proof_global.name ~typ:EConstr.mkSet ~impargs:[] in
+    let info = add_first_thm ~info ~name:proof.Declare.name ~typ:EConstr.mkSet ~impargs:[] in
     finalize_proof proof info
   else
     let info = process_idopt_for_save ~idopt info in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 8a23daa85f..f8e9e1f529 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -19,10 +19,10 @@ type t
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 (** [set_endline_tactic tac lemma] set ending tactic for [lemma] *)
 
-val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
+val pf_map : (Declare.t -> Declare.t) -> t -> t
 (** [pf_map f l] map the underlying proof object *)
 
-val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
+val pf_fold : (Declare.t -> 'a) -> t -> 'a
 (** [pf_fold f l] fold over the underlying proof object *)
 
 val by : unit Proofview.tactic -> t -> t * bool
@@ -101,21 +101,21 @@ val start_lemma_with_initialization
 val save_lemma_admitted : lemma:t -> unit
 val save_lemma_proved
   :  lemma:t
-  -> opaque:Proof_global.opacity_flag
+  -> opaque:Declare.opacity_flag
   -> idopt:Names.lident option
   -> unit
 
 (** To be removed, don't use! *)
 module Internal : sig
   val get_info : t -> Info.t
-  (** Only needed due to the Proof_global compatibility layer. *)
+  (** Only needed due to the Declare compatibility layer. *)
 end
 
 (** Special cases for delayed proofs, in this case we must provide the
    proof information so the proof won't be forced. *)
-val save_lemma_admitted_delayed : proof:Proof_global.proof_object -> info:Info.t -> unit
+val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit
 val save_lemma_proved_delayed
-  :  proof:Proof_global.proof_object
+  :  proof:Declare.proof_object
   -> info:Info.t
   -> idopt:Names.lident option
   -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e59c93c2e2..060f069419 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -134,7 +134,7 @@ let solve_by_tac ?loc name evi t poly uctx =
     (* the status is dropped. *)
     let env = Global.env () in
     let body, types, _, uctx =
-      Proof_global.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
+      Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
     Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
     Some (body, types, uctx)
   with
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index baaf8aa849..7a2e6d8b03 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -791,7 +791,7 @@ let string_of_definition_object_kind = let open Decls in function
         return (keyword "Admitted")
 
       | VernacEndProof (Proved (opac,o)) -> return (
-        let open Proof_global in
+        let open Declare in
         match o with
           | None -> (match opac with
               | Transparent -> keyword "Defined"
diff --git a/vernac/search.ml b/vernac/search.ml
index 1e89cbd551..8b54b696f2 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -61,7 +61,7 @@ let iter_named_context_name_type f =
 let get_current_or_goal_context ?pstate glnum =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Proof_global.get_goal_context p glnum
+  | Some p -> Declare.get_goal_context p glnum
 
 (* General search over hypothesis of a goal *)
 let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
diff --git a/vernac/search.mli b/vernac/search.mli
index 6dbbff3a8c..16fd303917 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -38,13 +38,13 @@ val search_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : ?pstate:Declare.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
+val search         : ?pstate:Declare.t -> int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -65,12 +65,12 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list ->
+val interface_search : ?pstate:Declare.t -> ?glnum:int -> (search_constraint * bool) list ->
   constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit
+val generic_search : ?pstate:Declare.t -> int option -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cbb578c109..37808a3726 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -34,12 +34,12 @@ let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Proof_global.get_current_context p
+  | Some p -> Declare.get_current_context p
 
 let get_goal_or_global_context ~pstate glnum =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Proof_global.get_goal_context p glnum
+  | Some p -> Declare.get_goal_context p glnum
 
 let cl_of_qualid = function
   | FunClass -> Coercionops.CL_FUN
@@ -94,13 +94,13 @@ let show_proof ~pstate =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   try
     let pstate = Option.get pstate in
-    let p = Proof_global.get_proof pstate in
-    let sigma, env = Proof_global.get_current_context pstate in
+    let p = Declare.get_proof pstate in
+    let sigma, env = Declare.get_current_context pstate in
     let pprf = Proof.partial_proof p in
     Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
   (* We print nothing if there are no goals left *)
   with
-  | Proof_global.NoSuchGoal
+  | Declare.NoSuchGoal
   | Option.IsNone ->
     user_err (str "No goals to show.")
 
@@ -476,7 +476,7 @@ let program_inference_hook env sigma ev =
     then None
     else
       let c, _, _, ctx =
-        Proof_global.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
+        Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
       in
       Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
   with
@@ -593,7 +593,7 @@ let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
-  let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
+  let () = Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -1167,7 +1167,7 @@ let focus_command_cond = Proof.no_cond command_focus
      all tactics fail if there are no further goals to prove. *)
 
 let vernac_solve_existential ~pstate n com =
-  Proof_global.map_proof (fun p ->
+  Declare.map_proof (fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -1175,12 +1175,12 @@ let vernac_set_end_tac ~pstate tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
-  Proof_global.set_endline_tactic tac pstate
+  Declare.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~pstate e : Proof_global.t =
+let vernac_set_used_variables ~pstate e : Declare.t =
   let env = Global.env () in
   let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
-  let tys = List.map snd (initial_goals (Proof_global.get_proof pstate)) in
+  let tys = List.map snd (initial_goals (Declare.get_proof pstate)) in
   let tys = List.map EConstr.Unsafe.to_constr tys in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
@@ -1189,7 +1189,7 @@ let vernac_set_used_variables ~pstate e : Proof_global.t =
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ Id.print id))
     l;
-  let _, pstate = Proof_global.set_used_variables pstate l in
+  let _, pstate = Declare.set_used_variables pstate l in
   pstate
 
 (*****************************)
@@ -1589,8 +1589,8 @@ let get_current_context_of_args ~pstate =
     let env = Global.env () in Evd.(from_env env, env)
   | Some lemma ->
     function
-    | Some n -> Proof_global.get_goal_context lemma n
-    | None -> Proof_global.get_current_context lemma
+    | Some n -> Declare.get_goal_context lemma n
+    | None -> Declare.get_current_context lemma
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1655,7 +1655,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal ~pstate n =
-  let pf = Proof_global.get_proof pstate in
+  let pf = Declare.get_proof pstate in
   let Proof.{goals;sigma} = Proof.data pf in
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
@@ -1690,7 +1690,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    let sigma, env = Proof_global.get_current_context pstate in
+    let sigma, env = Declare.get_current_context pstate in
     v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
          ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
@@ -1893,7 +1893,7 @@ let vernac_register qid r =
 (* Proof management *)
 
 let vernac_focus ~pstate gln =
-  Proof_global.map_proof (fun p ->
+  Declare.map_proof (fun p ->
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
@@ -1904,13 +1904,13 @@ let vernac_focus ~pstate gln =
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus ~pstate =
-  Proof_global.map_proof
+  Declare.map_proof
     (fun p -> Proof.unfocus command_focus p ())
     pstate
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused ~pstate =
-  let p = Proof_global.get_proof pstate in
+  let p = Declare.get_proof pstate in
   if Proof.unfocused p then
     str"The proof is indeed fully unfocused."
   else
@@ -1923,7 +1923,7 @@ let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln ~pstate =
-  Proof_global.map_proof (fun p ->
+  Declare.map_proof (fun p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
@@ -1933,12 +1933,12 @@ let vernac_subproof gln ~pstate =
     pstate
 
 let vernac_end_subproof ~pstate =
-  Proof_global.map_proof (fun p ->
+  Declare.map_proof (fun p ->
       Proof.unfocus subproof_kind p ())
     pstate
 
 let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
-  Proof_global.map_proof (fun p ->
+  Declare.map_proof (fun p ->
     Proof_bullet.put p bullet) pstate
 
 (* Stack is needed due to show proof names, should deprecate / remove
@@ -1955,7 +1955,7 @@ let vernac_show ~pstate =
     end
   (* Show functions that require a proof state *)
   | Some pstate ->
-    let proof = Proof_global.get_proof pstate in
+    let proof = Declare.get_proof pstate in
     begin function
     | ShowGoal goalref ->
       begin match goalref with
@@ -1967,14 +1967,14 @@ let vernac_show ~pstate =
     | ShowUniverses -> show_universes ~proof
     (* Deprecate *)
     | ShowProofNames ->
-      Id.print (Proof_global.get_proof_name pstate)
+      Id.print (Declare.get_proof_name pstate)
     | ShowIntros all -> show_intro ~proof all
     | ShowProof -> show_proof ~pstate:(Some pstate)
     | ShowMatch id -> show_match id
     end
 
 let vernac_check_guard ~pstate =
-  let pts = Proof_global.get_proof pstate in
+  let pts = Declare.get_proof pstate in
   let pfterm = List.hd (Proof.partial_proof pts) in
   let message =
     try
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 27663a0681..c32ac414ba 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -202,7 +202,7 @@ type syntax_modifier =
 type proof_end =
   | Admitted
   (*                         name in `Save ident` when closing goal *)
-  | Proved of Proof_global.opacity_flag * lident option
+  | Proved of Declare.opacity_flag * lident option
 
 type scheme =
   | InductionScheme of bool * qualid or_by_notation * sort_expr
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 1920c276af..03172b2700 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -57,9 +57,9 @@ type typed_vernac =
   | VtNoProof of (unit -> unit)
   | VtCloseProof of (lemma:Lemmas.t -> unit)
   | VtOpenProof of (unit -> Lemmas.t)
-  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
-  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
-  | VtReadProof of (pstate:Proof_global.t -> unit)
+  | VtModifyProof of (pstate:Declare.t -> Declare.t)
+  | VtReadProofOpt of (pstate:Declare.t option -> unit)
+  | VtReadProof of (pstate:Declare.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d0ebc1086..62136aa38d 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -75,9 +75,9 @@ type typed_vernac =
   | VtNoProof of (unit -> unit)
   | VtCloseProof of (lemma:Lemmas.t -> unit)
   | VtOpenProof of (unit -> Lemmas.t)
-  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
-  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
-  | VtReadProof of (pstate:Proof_global.t -> unit)
+  | VtModifyProof of (pstate:Declare.t -> Declare.t)
+  | VtReadProofOpt of (pstate:Declare.t option -> unit)
+  | VtReadProof of (pstate:Declare.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index eb299222dd..14f477663d 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -209,7 +209,7 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
        let before_univs = Global.universes () in
        let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
        if before_univs == Global.universes () then pstack
-       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
+       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Declare.update_global_env) pstack)
     ~st
 
 (* XXX: This won't properly set the proof mode, as of today, it is
@@ -251,7 +251,7 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
       let ontop = v_mod (interp_fn ~st) cmd in
-      Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
+      Vernacstate.Declare.set ontop [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
   with exn ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 9f5bfb46ee..e3e708e87d 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,7 +14,7 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
 (** Execute a Qed but with a proof_object which may contain a delayed
    proof and won't be forced *)
 val interp_qed_delayed_proof
-  :  proof:Proof_global.proof_object
+  :  proof:Declare.proof_object
   -> info:Lemmas.Info.t
   -> st:Vernacstate.t
   -> control:Vernacexpr.control_flag list
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 2987b3bc43..d1e0dce116 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -45,7 +45,7 @@ module LemmaStack = struct
     | Some (l,ls) -> a, (l :: ls)
 
   let get_all_proof_names (pf : t) =
-    let prj x = Lemmas.pf_fold Proof_global.get_proof x in
+    let prj x = Lemmas.pf_fold Declare.get_proof x in
     let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
     pn :: pns
 
@@ -105,7 +105,7 @@ let make_shallow st =
   }
 
 (* Compatibility module *)
-module Proof_global = struct
+module Declare = struct
 
   let get () = !s_lemmas
   let set x = s_lemmas := x
@@ -126,7 +126,7 @@ module Proof_global = struct
     end
 
   open Lemmas
-  open Proof_global
+  open Declare
 
   let cc f = match !s_lemmas with
     | None -> raise NoCurrentProof
@@ -161,7 +161,7 @@ module Proof_global = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
+  type closed_proof = Declare.proof_object * Lemmas.Info.t
 
 
   let return_proof () = cc return_proof
@@ -169,16 +169,16 @@ module Proof_global = struct
 
   let close_future_proof ~feedback_id pf =
     cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt,
-                        Internal.get_info pt)
+                        Lemmas.Internal.get_info pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate =
     cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt,
-                        Internal.get_info pt)
+                        Lemmas.Internal.get_info pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
 
-  let get_current_context () = cc Proof_global.get_current_context
+  let get_current_context () = cc Declare.get_current_context
 
   let get_all_proof_names () =
     try cc_stack LemmaStack.get_all_proof_names
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 9c4de7720c..2cabbe35f5 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -25,8 +25,8 @@ module LemmaStack : sig
   val pop : t -> Lemmas.t * t option
   val push : t option -> Lemmas.t -> t
 
-  val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
-  val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
+  val map_top_pstate : f:(Declare.t -> Declare.t) -> t -> t
+  val with_top_pstate : t -> f:(Declare.t -> 'a ) -> 'a
 
 end
 
@@ -50,7 +50,7 @@ val make_shallow : t -> t
 val invalidate_cache : unit -> unit
 
 (* Compatibility module: Do Not Use *)
-module Proof_global : sig
+module Declare : sig
 
   exception NoCurrentProof
 
@@ -65,16 +65,16 @@ module Proof_global : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val return_proof : unit -> Proof_global.closed_proof_output
-  val return_partial_proof : unit -> Proof_global.closed_proof_output
+  val return_proof : unit -> Declare.closed_proof_output
+  val return_partial_proof : unit -> Declare.closed_proof_output
 
-  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
+  type closed_proof = Declare.proof_object * Lemmas.Info.t
 
   val close_future_proof :
     feedback_id:Stateid.t ->
-    Proof_global.closed_proof_output Future.computation -> closed_proof
+    Declare.closed_proof_output Future.computation -> closed_proof
 
-  val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
+  val close_proof : opaque:Declare.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
 
   val discard_all : unit -> unit
   val update_global_env : unit -> unit
@@ -89,7 +89,7 @@ module Proof_global : sig
   val get : unit -> LemmaStack.t option
   val set : LemmaStack.t option -> unit
 
-  val get_pstate : unit -> Proof_global.t option
+  val get_pstate : unit -> Declare.t option
 
   val freeze : marshallable:bool -> LemmaStack.t option
   val unfreeze : LemmaStack.t -> unit