Merge PR #11999: [proof] Merge `Proof_global` into `Declare`

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: ppedrot

57 files changed, 977 insertions, 972 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eac8d86b0a..9498ab8bbb 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,13 @@
 
 ### ML API
 
+Proof state and constant declaration:
+
+- A large consolidation of the API handling interactive and
+  non-interactive constant has been performed; low-level APIs are no
+  longer available, and the functionality of the `Proof_global` module
+  has been merged into `Declare`.
+
 Notations:
 
 - Most operators on numerals have moved to file numTok.ml.
@@ -68,7 +75,6 @@ Proof state:
   information related to the constant declaration. Some functions have
   been renamed from `start_proof` to `start_lemma`
 
-
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7002cbffac..542893ad0b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,8 +59,8 @@ let prrecarg = function
 let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 
 let get_current_context () =
-  try Vernacstate.Proof_global.get_current_context ()
-  with Vernacstate.Proof_global.NoCurrentProof ->
+  try Vernacstate.Declare.get_current_context ()
+  with Vernacstate.Declare.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
   [@@ocaml.warning "-3"]
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 73d94c2a51..8c2090f3be 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,8 +286,8 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Pfedit.get_current_context pstate in
-    let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in
+    let sigma, env = Declare.get_current_context pstate in
+    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 0ef7fca41f..fa458e7c6e 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -232,32 +232,32 @@ let goals () =
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let newp = Vernacstate.Proof_global.give_me_the_proof () in
+    let newp = Vernacstate.Declare.give_me_the_proof () in
     if Proof_diffs.show_diffs () then begin
       let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
       let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
       Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
     end else
       Some (export_pre_goals Proof.(data newp) process_goal)
-  with Vernacstate.Proof_global.NoCurrentProof -> None
+  with Vernacstate.Declare.NoCurrentProof -> None
   [@@ocaml.warning "-3"];;
 
 let evars () =
   try
     let doc = get_doc () in
     set_doc @@ Stm.finish ~doc;
-    let pfts = Vernacstate.Proof_global.give_me_the_proof () in
+    let pfts = Vernacstate.Declare.give_me_the_proof () in
     let Proof.{ sigma } = Proof.data pfts in
     let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
     let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
     let el = List.map map_evar exl in
     Some el
-  with Vernacstate.Proof_global.NoCurrentProof -> None
+  with Vernacstate.Declare.NoCurrentProof -> None
   [@@ocaml.warning "-3"]
 
 let hints () =
   try
-    let pfts = Vernacstate.Proof_global.give_me_the_proof () in
+    let pfts = Vernacstate.Declare.give_me_the_proof () in
     let Proof.{ goals; sigma } = Proof.data pfts in
     match goals with
     | [] -> None
@@ -266,7 +266,7 @@ let hints () =
       let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
       let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
       Some (hint_hyps, concl_next_tac)
-  with Vernacstate.Proof_global.NoCurrentProof -> None
+  with Vernacstate.Declare.NoCurrentProof -> None
   [@@ocaml.warning "-3"]
 
 (** Other API calls *)
@@ -287,11 +287,11 @@ let status force =
     List.rev_map Names.Id.to_string l
   in
   let proof =
-    try Some (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ()))
-    with Vernacstate.Proof_global.NoCurrentProof -> None
+    try Some (Names.Id.to_string (Vernacstate.Declare.get_current_proof_name ()))
+    with Vernacstate.Declare.NoCurrentProof -> None
   in
   let allproofs =
-    let l = Vernacstate.Proof_global.get_all_proof_names () in
+    let l = Vernacstate.Declare.get_all_proof_names () in
     List.map Names.Id.to_string l
   in
   {
@@ -340,7 +340,7 @@ let import_search_constraint = function
   | Interface.Include_Blacklist -> Search.Include_Blacklist
 
 let search flags =
-  let pstate = Vernacstate.Proof_global.get_pstate () in
+  let pstate = Vernacstate.Declare.get_pstate () in
   List.map export_coq_object (Search.interface_search ?pstate (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index dca69f06ca..f09b35a6d1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -42,6 +42,6 @@ let start_deriving f suchthat name : Lemmas.t =
 
   let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
   let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
-  Lemmas.pf_map (Proof_global.map_proof begin fun p ->
+  Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3a90d24c97..02383799a9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -728,13 +728,13 @@ let extract_and_compile l =
 (* Show the extraction of the current ongoing proof *)
 let show_extraction ~pstate =
   init ~inner:true false false;
-  let prf = Proof_global.get_proof pstate in
-  let sigma, env = Pfedit.get_current_context pstate in
+  let prf = Declare.Proof.get_proof pstate in
+  let sigma, env = Declare.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
-    let l = Label.of_id (Proof_global.get_proof_name pstate) in
+    let l = Label.of_id (Declare.Proof.get_proof_name pstate) in
     let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index edbc1f5ea7..06cc475200 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
 
 (* Show the extraction of the current ongoing proof *)
 
-val show_extraction : pstate:Proof_global.t -> unit
+val show_extraction : pstate:Declare.Proof.t -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ad0891b567..7b2ce671a3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -847,7 +847,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   in
   let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
+    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index df147b3aa6..eec78391af 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -191,7 +191,7 @@ let prepare_body {Vernacexpr.binders} rt =
   let fun_args, rt' = chop_rlambda_n n rt in
   (fun_args, rt')
 
-let build_functional_principle ?(opaque = Proof_global.Transparent)
+let build_functional_principle ?(opaque = Declare.Transparent)
     (evd : Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams =
@@ -233,9 +233,10 @@ let build_functional_principle ?(opaque = Proof_global.Transparent)
   (*      let dur1 = System.time_difference tim1 tim2 in *)
   (*      Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
   (*    end; *)
-  let open Proof_global in
-  let {entries} =
-    Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma
+  let {Declare.entries} =
+    Lemmas.pf_fold
+      (Declare.close_proof ~opaque ~keep_body_ucst_separate:false)
+      lemma
   in
   match entries with
   | [entry] -> (entry, hook)
@@ -1394,7 +1395,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
       | None -> raise Not_found
       | Some finfos -> finfos
     in
-    let open Proof_global in
+    let open Declare in
     match finfos.equation_lemma with
     | None -> Transparent (* non recursive definition *)
     | Some equation ->
@@ -1550,7 +1551,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent
+            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1621,7 +1622,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent
+            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bd19648c08..ffb9a7e69b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -27,7 +27,6 @@ open Tacticals
 open Tacmach
 open Tactics
 open Nametab
-open Declare
 open Tacred
 open Glob_term
 open Pretyping
@@ -54,11 +53,12 @@ let find_reference sl s =
   locate (make_qualid dp (Id.of_string s))
 
 let declare_fun name kind ?univs value =
-  let ce = definition_entry ?univs value (*FIXME *) in
-  GlobRef.ConstRef (declare_constant ~name ~kind (DefinitionEntry ce))
+  let ce = Declare.definition_entry ?univs value (*FIXME *) in
+  GlobRef.ConstRef
+    (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
+  Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1336,7 +1336,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
     g
 
 let get_current_subgoals_types pstate =
-  let p = Proof_global.get_proof pstate in
+  let p = Declare.Proof.get_proof pstate in
   let Proof.{goals = sgs; sigma; _} = Proof.data p in
   (sigma, List.map (Goal.V82.abstract_type sigma) sgs)
 
@@ -1408,15 +1408,15 @@ let build_new_goal_type lemma =
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
   match cb.Declarations.const_body with
-  | Declarations.OpaqueDef _ -> Proof_global.Opaque
-  | Declarations.Undef _ -> Proof_global.Opaque
-  | Declarations.Def _ -> Proof_global.Transparent
-  | Declarations.Primitive _ -> Proof_global.Opaque
+  | Declarations.OpaqueDef _ -> Declare.Opaque
+  | Declarations.Undef _ -> Declare.Opaque
+  | Declarations.Def _ -> Declare.Transparent
+  | Declarations.Primitive _ -> Declare.Opaque
 
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Lemmas.pf_fold Proof_global.get_proof_name lemma in
+  let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
   let name =
     match goal_name with
     | Some s -> s
@@ -1514,7 +1514,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                   g))
            lemma
   in
-  if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (
+  if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
     defined lemma; None )
   else Some lemma
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7b1aa7a07a..7754fe401e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -346,7 +346,7 @@ open Vars
 
 let constr_flags () = {
   Pretyping.use_typeclasses = Pretyping.UseTC;
-  Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+  Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
@@ -918,7 +918,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Proof_global.map_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Declare.Proof.map_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Proof_global.compact_the_proof pstate }
+  { fun ~pstate -> Declare.Proof.compact pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 2bd4211c90..e713ab13b2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -364,12 +364,12 @@ let print_info_trace =
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info (print_info_trace ()) in
       let (p,status) =
-        Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+        Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
       in
       (* in case a strict subtree was completed,
          go back to the top of the prooftree *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..820063c25c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
         let name, poly = Id.of_string "rewrite", false in
-        let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+        let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
         Evd.define evk (EConstr.of_constr c) sigma
     in
     List.fold_left solve sigma indep
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b0e26e1def..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2070,7 +2070,7 @@ let _ =
      *)
     let name, poly = Id.of_string "ltac_gen", poly in
     let name, poly = Id.of_string "ltac_gen", poly in
-    let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 21006349d2..75aca7e7ff 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,7 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
-exception NoSuchGoal of Names.Id.t
+exception NoSuchGoal of Names.Id.t option
 
 exception FullyUnfocused
 
@@ -74,8 +74,10 @@ let _ = CErrors.register_handler begin function
     Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
     Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
-  | NoSuchGoal id ->
+  | NoSuchGoal (Some id) ->
     Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+  | NoSuchGoal None ->
+    Some Pp.(str "[Focus] No such goal.")
   | FullyUnfocused ->
     Some (Pp.str "The proof is not focused")
   | _ -> None
@@ -233,7 +235,7 @@ let focus_id cond inf id pr =
           raise CannotUnfocusThisWay
      end
   | None ->
-     raise (NoSuchGoal id)
+     raise (NoSuchGoal (Some id))
   end
 
 let rec unfocus kind pr () =
@@ -506,3 +508,124 @@ let pr_proof p =
     str "given up: " ++ pr_goal_list given_up ++
     str "]"
   )
+
+let use_unification_heuristics =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Solve";"Unification";"Constraints"]
+    ~value:true
+
+exception SuggestNoSuchGoals of int * t
+
+let solve ?with_end_tac gi info_lvl tac pr =
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace tac
+    in
+    let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
+      | SelectAll -> tac
+    in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
+    let env = Global.env () in
+    let (p,(status,info),()) = run_tactic env tac pr in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Feedback.msg_info (Pp.hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
+    in
+    (p,status)
+
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+let refine_by_tactic ~name ~poly env sigma ty tac =
+  (* Save the initial side-effects to restore them afterwards. We set the
+     current set of side-effects to be empty so that we can retrieve the
+     ones created during the tactic invocation easily. *)
+  let eff = Evd.eval_side_effects sigma in
+  let sigma = Evd.drop_side_effects sigma in
+  (* Save the existing goals *)
+  let prev_future_goals = Evd.save_future_goals sigma in
+  (* Start a proof *)
+  let prf = start ~name ~poly sigma [env, ty] in
+  let (prf, _, ()) =
+    try run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (* Catch the inner error of the monad tactic *)
+      let (_, info) = Exninfo.capture src in
+      Exninfo.iraise (e, info)
+  in
+  (* Plug back the retrieved sigma *)
+  let { goals; stack; shelf; given_up; sigma; entry } = data prf in
+  assert (stack = []);
+  let ans = match Proofview.initial_goals entry with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
+  (* [neff] contains the freshly generated side-effects *)
+  let neff = Evd.eval_side_effects sigma in
+  (* Reset the old side-effects *)
+  let sigma = Evd.drop_side_effects sigma in
+  let sigma = Evd.emit_side_effects eff sigma in
+  (* Restore former goals *)
+  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  (* Push remaining goals as future_goals which is the only way we
+     have to inform the caller that there are goals to collect while
+     not being encapsulated in the monad *)
+  (* Goals produced by tactic "shelve" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+  (* Goals produced by tactic "give_up" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+  (* Other goals *)
+  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
+  (* Get rid of the fresh side-effects by internalizing them in the term
+     itself. Note that this is unsound, because the tactic may have solved
+     other goals that were already present during its invocation, so that
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
+  let neff = neff.Evd.seff_private in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
+  ans, sigma
+
+let get_nth_V82_goal p i =
+  let { sigma; goals } = data p in
+  try { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise (NoSuchGoal None)
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Global.env_of_context (Goal.V82.hyps sigma goal))
+
+let get_proof_context p =
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal _ ->
+    (* No more focused goals *)
+    let { sigma } = data p in
+    sigma, Global.env ()
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1a0b105723..0e5bdaf07d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -143,6 +143,8 @@ exception CannotUnfocusThisWay
    Bullet.push. *)
 exception NoSuchGoals of int * int
 
+exception NoSuchGoal of Names.Id.t option
+
 (* Unfocusing command.
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
@@ -207,3 +209,41 @@ end
 
 (* returns the set of all goals in the proof *)
 val all_goals : t -> Goal.Set.t
+
+(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
+    subgoal of the current focused proof. [solve SelectAll
+    tac] applies [tac] to all subgoals. *)
+
+val solve :
+     ?with_end_tac:unit Proofview.tactic
+  -> Goal_select.t
+  -> int option
+  -> unit Proofview.tactic
+  -> t
+  -> t * bool
+
+(** Option telling if unification heuristics should be used. *)
+val use_unification_heuristics : unit -> bool
+
+val refine_by_tactic
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+    Caveat: all effects are purged in the returned term at the end, but other
+    evars solved by side-effects are NOT purged, so that unexpected failures may
+    occur. Ideally all code using this function should be rewritten in the
+    monad. *)
+
+exception SuggestNoSuchGoals of int * t
+
+(** {6 Helpers to obtain proof state when in an interactive proof } *)
+val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_context : t -> Evd.evar_map * Environ.env
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index f619bc86a1..41cb7399da 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -191,11 +191,8 @@ let put p b =
 let suggest p =
   (current_behavior ()).suggest p
 
-(* Better printing for bullet exceptions *)
-exception SuggestNoSuchGoals of int * Proof.t
-
 let _ = CErrors.register_handler begin function
-    | SuggestNoSuchGoals(n,proof) ->
+    | Proof.SuggestNoSuchGoals(n,proof) ->
       let suffix = suggest proof in
       Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
                 pr_non_empty_arg (fun x -> x) suffix))
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 687781361c..f15b7824ff 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,5 +44,3 @@ val register_behavior : behavior -> unit
      *)
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
-
-exception SuggestNoSuchGoals of int * Proof.t
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 6a78dd5529..2ff76e69f8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -50,7 +50,7 @@ let is_focused_goal_simple ~doc id =
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.lemmas }) ->
     Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
-        let proof = Proof_global.get_proof proof in
+        let proof = Declare.Proof.get_proof proof in
         let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
         let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
         if List.for_all (fun x -> simple_goal sigma x rest) focused
diff --git a/stm/stm.ml b/stm/stm.ml
index 5b88ee3d68..f3768e9b99 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -27,7 +27,7 @@ open Feedback
 open Vernacexpr
 open Vernacextend
 
-module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"]
+module PG_compat = Vernacstate.Declare [@@ocaml.warning "-3"]
 
 let is_vtkeep = function VtKeep _ -> true | _ -> false
 let get_vtkeep = function VtKeep x -> x | _ -> assert false
@@ -147,7 +147,7 @@ let update_global_env () =
     PG_compat.update_global_env ()
 
 module Vcs_ = Vcs.Make(Stateid.Self)
-type future_proof = Proof_global.closed_proof_output Future.computation
+type future_proof = Declare.closed_proof_output Future.computation
 
 type depth = int
 type branch_type =
@@ -1164,7 +1164,7 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas
+    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
@@ -1358,7 +1358,7 @@ module rec ProofTask : sig
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1381,7 +1381,7 @@ module rec ProofTask : sig
     ?loc:Loc.t ->
     drop_pt:bool ->
     Stateid.t * Stateid.t -> Stateid.t ->
-      Proof_global.closed_proof_output Future.computation
+      Declare.closed_proof_output Future.computation
 
   (* If set, only tasks overlapping with this list are processed *)
   val set_perspective : Stateid.t list -> unit
@@ -1397,7 +1397,7 @@ end = struct (* {{{ *)
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Proof_global.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.closed_proof_output Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1419,7 +1419,7 @@ end = struct (* {{{ *)
     e_safe_states : Stateid.t list }
 
   type response =
-    | RespBuiltProof of Proof_global.closed_proof_output * float
+    | RespBuiltProof of Declare.closed_proof_output * float
     | RespError of error
     | RespStates of (Stateid.t * State.partial_state) list
 
@@ -1530,7 +1530,7 @@ end = struct (* {{{ *)
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
-          let opaque = Proof_global.Opaque in
+          let opaque = Declare.Opaque in
           stm_qed_delay_proof ~st ~id:stop
             ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
         ignore(Future.join checked_proof);
@@ -1664,7 +1664,7 @@ end = struct (* {{{ *)
         let _proof = PG_compat.return_partial_proof () in
         `OK_ADMITTED
       else begin
-      let opaque = Proof_global.Opaque in
+      let opaque = Declare.Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
       let proof, _info =
@@ -1723,7 +1723,7 @@ end = struct (* {{{ *)
     | `ERROR -> exit 1
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
-    | `OK { Proof_global.name } ->
+    | `OK { Declare.name } ->
         let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
@@ -2149,7 +2149,7 @@ let collect_proof keep cur hd brkind id =
    | id :: _ -> Names.Id.to_string id in
  let loc = (snd cur).expr.CAst.loc in
  let is_defined_expr = function
-   | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
+   | VernacEndProof (Proved (Declare.Transparent,_)) -> true
    | _ -> false in
  let is_defined = function
    | _, { expr = e } -> is_defined_expr e.CAst.v.expr
@@ -2310,7 +2310,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                Option.iter PG_compat.unfreeze lemmas;
                PG_compat.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
-                 fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
+                 fst (Proof.solve Goal_select.SelectAll None tac p), ());
                (* STATE SPEC:
                 * - start: Modifies the input state adding a proof.
                 * - end  : maybe after recovery command.
@@ -2514,7 +2514,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                   | VtKeep VtKeepAxiom ->
                       qed.fproof <- Some (None, ref false); None
                   | VtKeep opaque ->
-                    let opaque = let open Proof_global in  match opaque with
+                    let opaque = let open Declare in  match opaque with
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
                       | VtKeepAxiom -> assert false
                     in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 567acb1c73..cf127648b4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification = function
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
 
-let vtkeep_of_opaque = let open Proof_global in function
+let vtkeep_of_opaque = let open Declare in function
   | Opaque -> VtKeepOpaque
   | Transparent -> VtKeepDefined
 
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e85d94cd72..0e78a03f45 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -11,7 +11,6 @@
 open Util
 open Termops
 open EConstr
-open Evarutil
 
 module NamedDecl = Context.Named.Declaration
 
@@ -76,61 +75,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
               | None ->  Proofview.Goal.concl gl
               | Some ty -> ty in
   let concl = it_mkNamedProd_or_LetIn concl sign in
-  let concl =
-    try flush_and_check_evars sigma concl
-    with Uninstantiated_evar _ ->
-      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in
-
-  let sigma, ctx, concl =
-    (* FIXME: should be done only if the tactic succeeds *)
-    let sigma = Evd.minimize_universes sigma in
-    let ctx = Evd.universe_context_set sigma in
-    sigma, ctx, Evarutil.nf_evars_universes sigma concl
-  in
-  let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
-  let ectx = Evd.evar_universe_context sigma in
-  let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac
-    with Logic_monad.TacticFailure e as src ->
-    (* if the tactic [tac] fails, it reports a [TacticFailure e],
-       which is an error irrelevant to the proof system (in fact it
-       means that [e] comes from [tac] failing to yield enough
-       success). Hence it reraises [e]. *)
-    let (_, info) = Exninfo.capture src in
-    Exninfo.iraise (e, info)
-  in
-  let body, effs = Future.force const.Declare.proof_entry_body in
-  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
-  let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in
-  (* EJGA: Hack related to the above call to
-     `build_constant_by_tactic` with `~opaque:Transparent`. Even if
-     the abstracted term is destined to be opaque, if we trigger the
-     `if poly && opaque && private_poly_univs ()` in `Proof_global`
-     kernel will boom. This deserves more investigation. *)
-  let const = Declare.Internal.set_opacity ~opaque const in
-  let const, args = Declare.Internal.shrink_entry sign const in
-  let args = List.map EConstr.of_constr args in
-  let cst () =
-    (* do not compute the implicit arguments, it may be costly *)
-    let () = Impargs.make_implicit_args false in
-    (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const
-  in
-  let cst, eff = Impargs.with_implicit_protection cst () in
-  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.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 sigma = Evd.set_universe_context sigma ectx in
-  let effs = Evd.concat_side_effects eff effs in
+  let effs, sigma, lem, args, safe =
+    Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 5135d72f7b..cce43e833e 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -13,11 +13,112 @@
 open Pp
 open Util
 open Names
-open Declarations
-open Entries
 open Safe_typing
-open Libobject
-open Lib
+module NamedDecl = Context.Named.Declaration
+
+type opacity_flag = Opaque | Transparent
+
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Id.Set.t option
+  ; proof : Proof.t
+  ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  }
+
+(*** Proof Global manipulation ***)
+
+let get_proof ps = ps.proof
+let get_proof_name ps = (Proof.data ps.proof).Proof.name
+
+let get_initial_euctx ps = ps.initial_euctx
+
+let map_proof f p = { p with proof = f p.proof }
+let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
+
+let map_fold_proof_endline f ps =
+  let et =
+    match ps.endline_tactic with
+    | None -> Proofview.tclUNIT ()
+    | Some tac ->
+      let open Geninterp in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
+      let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+      let tac = Geninterp.interp tag ist tac in
+      Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+  in
+  let (newpr,ret) = f et ps.proof in
+  let ps = { ps with proof = newpr } in
+  ps, ret
+
+let compact_the_proof pf = map_proof Proof.compact pf
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac ps =
+  { ps with endline_tactic = Some tac }
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion). The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
+  let proof = Proof.start ~name ~poly sigma goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; udecl
+  ; initial_euctx
+  }
+
+let start_dependent_proof ~name ~udecl ~poly goals =
+  let proof = Proof.dependent_start ~name ~poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
+  ; endline_tactic = None
+  ; section_vars = None
+  ; udecl
+  ; initial_euctx
+  }
+
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.udecl
+
+let set_used_variables ps l =
+  let open Context.Named.Declaration in
+  let env = Global.env () in
+  let ids = List.fold_right Id.Set.add l Id.Set.empty in
+  let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe as orig) =
+    match entry with
+    | LocalAssum ({Context.binder_name=x},_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe)
+    | LocalDef ({Context.binder_name=x},bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe)
+       else (ctx, all_safe) in
+  let ctx, _ =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
+  if not (Option.is_empty ps.section_vars) then
+    CErrors.user_err Pp.(str "Used section variables can be declared only once");
+  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+
+let get_open_goals ps =
+  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+  List.length goals +
+  List.fold_left (+) 0
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
+  List.length shelf
 
 (* object_kind , id *)
 exception AlreadyDeclared of (string option * Id.t)
@@ -30,8 +131,6 @@ let _ = CErrors.register_handler (function
     | _ ->
       None)
 
-module NamedDecl = Context.Named.Declaration
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Monomorphic universes need to survive sections. *)
@@ -78,10 +177,118 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
+let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
+
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
+  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
+    proof_entry_secctx = section_vars;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = feedback_id;
+    proof_entry_inline_code = inline}
+
+type proof_object =
+  { name : Names.Id.t
+  (* [name] only used in the STM *)
+  ; entries : Evd.side_effects proof_entry list
+  ; uctx: UState.t
+  }
+
+let private_poly_univs =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Private";"Polymorphic";"Universes"]
+    ~value:true
+
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
+let prepare_proof ~unsafe_typ { proof } =
+  let Proof.{name=pid;entry;poly} = Proof.data proof in
+  let initial_goals = Proofview.initial_goals entry in
+  let evd = Proof.return ~pid proof in
+  let eff = Evd.eval_side_effects evd in
+  let evd = Evd.minimize_universes evd in
+  let to_constr_body c =
+    match EConstr.to_constr_opt evd c with
+    | Some p -> p
+    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  in
+  let to_constr_typ t =
+    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+  in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
+  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
+  proofs, Evd.evar_universe_context evd
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly } = Proof.data proof in
+  let unsafe_typ = keep_body_ucst_separate && not poly in
+  let elist, uctx = prepare_proof ~unsafe_typ ps in
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
+
+  let make_entry ((body, eff), typ) =
+
+    let allow_deferred =
+      not poly &&
+      (keep_body_ucst_separate
+       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+    in
+    let used_univs_body = Vars.universes_of_constr body in
+    let used_univs_typ = Vars.universes_of_constr typ in
+    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+    let utyp, ubody =
+      if allow_deferred then
+        let utyp = UState.univ_entry ~poly initial_euctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        (* For vi2vo compilation proofs are computed now but we need to
+           complement the univ constraints of the typ with the ones of
+           the body.  So we keep the two sets distinct. *)
+        let uctx_body = UState.restrict uctx used_univs in
+        let ubody = UState.check_mono_univ_decl uctx_body udecl in
+        utyp, ubody
+      else if poly && opaque && private_poly_univs () then
+        let universes = UState.restrict uctx used_univs in
+        let typus = UState.restrict universes used_univs_typ in
+        let utyp = UState.check_univ_decl ~poly typus udecl in
+        let ubody = Univ.ContextSet.diff
+            (UState.context_set universes)
+            (UState.context_set typus)
+        in
+        utyp, ubody
+      else
+        (* Since the proof is computed now, we can simply have 1 set of
+           constraints in which we merge the ones for the body and the ones
+           for the typ. We recheck the declaration after restricting with
+           the actually used universes.
+           TODO: check if restrict is really necessary now. *)
+        let ctx = UState.restrict uctx used_univs in
+        let utyp = UState.check_univ_decl ~poly ctx udecl in
+        utyp, Univ.ContextSet.empty
+    in
+    definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+  in
+  let entries = CList.map make_entry elist  in
+  { name; entries; uctx }
+
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
-  | ParameterEntry of parameter_entry
-  | PrimitiveEntry of primitive_entry
+  | ParameterEntry of Entries.parameter_entry
+  | PrimitiveEntry of Entries.primitive_entry
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -99,7 +306,7 @@ let open_constant f i ((sp,kn), obj) =
   | ImportNeedQualified -> ()
   | ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
-    if in_filter_ref (GlobRef.ConstRef con) f then
+    if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
       Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
 
 let exists_name id =
@@ -130,9 +337,10 @@ let dummy_constant cst = {
   cst_locl = cst.cst_locl;
 }
 
-let classify_constant cst = Substitute (dummy_constant cst)
+let classify_constant cst = Libobject.Substitute (dummy_constant cst)
 
 let (objConstant : constant_obj Libobject.Dyn.tag) =
+  let open Libobject in
   declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -153,7 +361,7 @@ let register_constant kn kind local =
     cst_locl = local;
   } in
   let id = Label.to_id (Constant.label kn) in
-  let _ = add_leaf id o in
+  let _ = Lib.add_leaf id o in
   update_tables kn
 
 let register_side_effect (c, role) =
@@ -186,18 +394,6 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
-
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
-    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
-  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
-    proof_entry_secctx = section_vars;
-    proof_entry_type = types;
-    proof_entry_universes = univs;
-    proof_entry_opaque = opaque;
-    proof_entry_feedback = feedback_id;
-    proof_entry_inline_code = inline}
-
 let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) body =
   { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
@@ -208,14 +404,14 @@ let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     proof_entry_feedback = None;
     proof_entry_inline_code = inline}
 
-let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body =
+let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
   { proof_entry_body = body
   ; proof_entry_secctx = section_vars
   ; proof_entry_type = types
   ; proof_entry_universes = univs
   ; proof_entry_opaque = opaque
   ; proof_entry_feedback = feedback_id
-  ; proof_entry_inline_code = inline
+  ; proof_entry_inline_code = false
   }
 
 let cast_proof_entry e =
@@ -223,14 +419,13 @@ let cast_proof_entry e =
   let univs =
     if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
     else match e.proof_entry_universes with
-      | Monomorphic_entry ctx' ->
+      | Entries.Monomorphic_entry ctx' ->
         (* This can actually happen, try compiling EqdepFacts for instance *)
-        Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
-      | Polymorphic_entry _ ->
+        Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
+      | Entries.Polymorphic_entry _ ->
         CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
   in
-  {
-    const_entry_body = body;
+  { Entries.const_entry_body = body;
     const_entry_secctx = e.proof_entry_secctx;
     const_entry_feedback = e.proof_entry_feedback;
     const_entry_type = e.proof_entry_type;
@@ -242,7 +437,7 @@ type ('a, 'b) effect_entry =
 | EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
 | PureEntry : (unit, Constr.constr) effect_entry
 
-let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry =
+let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b Entries.opaque_entry =
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
@@ -276,16 +471,16 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
   | PureEntry ->
     let (body, uctx), () = Future.force e.proof_entry_body in
     let univs = match e.proof_entry_universes with
-    | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx')
-    | Polymorphic_entry _ ->
+    | Entries.Monomorphic_entry uctx' ->
+      Entries.Monomorphic_entry (Univ.ContextSet.union uctx uctx')
+    | Entries.Polymorphic_entry _ ->
       assert (Univ.ContextSet.is_empty uctx);
       e.proof_entry_universes
     in
     body, univs
   | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
   in
-  {
-    opaque_entry_body = body;
+  { Entries.opaque_entry_body = body;
     opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
@@ -295,6 +490,7 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags () =
+  let open Declarations in
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
@@ -366,6 +562,7 @@ type variable_declaration =
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
 let objVariable : unit Libobject.Dyn.tag =
+  let open Libobject in
   declare_object_full { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
@@ -386,15 +583,15 @@ let declare_variable ~name ~kind d =
       let ((body, body_ui), eff) = Future.force de.proof_entry_body in
       let () = export_side_effects eff in
       let poly, entry_ui = match de.proof_entry_universes with
-        | Monomorphic_entry uctx -> false, uctx
-        | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+        | Entries.Monomorphic_entry uctx -> false, uctx
+        | Entries.Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = declare_universe_context ~poly univs in
       let se = {
-        secdef_body = body;
+        Entries.secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
         secdef_feedback = de.proof_entry_feedback;
         secdef_type = de.proof_entry_type;
@@ -404,7 +601,7 @@ let declare_variable ~name ~kind d =
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
-  ignore(add_leaf name (inVariable ()) : Libobject.object_name);
+  ignore(Lib.add_leaf name (inVariable ()) : Libobject.object_name);
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
@@ -511,3 +708,194 @@ module Internal = struct
   let objConstant = objConstant
 
 end
+(*** Proof Global Environment ***)
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+  let fpl, uctx = Future.split2 fpl in
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k = Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
+
+  (* We only support opaque proofs, this will be enforced by using
+     different entries soon *)
+  let opaque = true in
+  let make_entry p (_, types) =
+    (* Already checked the univ_decl for the type universes when starting the proof. *)
+    let univs = UState.univ_entry ~poly:false initial_euctx in
+    let types = nf (EConstr.Unsafe.to_constr types) in
+
+    Future.chain p (fun (pt,eff) ->
+        (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+        let uctx = Future.force uctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        let used_univs = Univ.LSet.union
+            (Vars.universes_of_constr types)
+            (Vars.universes_of_constr pt)
+        in
+        let univs = UState.restrict uctx used_univs in
+        let univs = UState.check_mono_univ_decl univs udecl in
+        (pt,univs),eff)
+    |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+  in
+  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx = initial_euctx }
+
+let close_future_proof = close_proof_delayed
+
+let return_partial_proof { proof } =
+ let proofs = Proof.partial_proof proof in
+ let Proof.{sigma=evd} = Proof.data proof in
+ let eff = Evd.eval_side_effects evd in
+ (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
+
+let return_proof ps =
+  let p, uctx = prepare_proof ~unsafe_typ:false ps in
+  List.map fst p, uctx
+
+let update_global_env =
+  map_proof (fun p ->
+      let { Proof.sigma } = Proof.data p in
+      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
+      p)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
+
+let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
+  let evd = Evd.from_ctx uctx in
+  let goals = [ (Global.env_of_context sign , typ) ] in
+  let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
+  let pf, status = by tac pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+  match entries with
+  | [entry] ->
+    entry, status, uctx
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
+
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+  let sign = Environ.(val_of_named_context (named_context env)) in
+  let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+  let cb, uctx =
+    if side_eff then inline_private_constants ~uctx env ce
+    else
+      (* GG: side effects won't get reset: no need to treat their universes specially *)
+      let (cb, ctx), _eff = Future.force ce.proof_entry_body in
+      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
+  in
+  cb, ce.proof_entry_type, status, univs
+
+let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
+  (* EJGA: flush_and_check_evars is only used in abstract, could we
+     use a different API? *)
+  let concl =
+    try Evarutil.flush_and_check_evars sigma concl
+    with Evarutil.Uninstantiated_evar _ ->
+      CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
+  in
+  let sigma, concl =
+    (* FIXME: should be done only if the tactic succeeds *)
+    let sigma = Evd.minimize_universes sigma in
+    sigma, Evarutil.nf_evars_universes sigma concl
+  in
+  let concl = EConstr.of_constr concl in
+  let uctx = Evd.evar_universe_context sigma in
+  let (const, safe, uctx) =
+    try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac
+    with Logic_monad.TacticFailure e as src ->
+    (* if the tactic [tac] fails, it reports a [TacticFailure e],
+       which is an error irrelevant to the proof system (in fact it
+       means that [e] comes from [tac] failing to yield enough
+       success). Hence it reraises [e]. *)
+    let (_, info) = Exninfo.capture src in
+    Exninfo.iraise (e, info)
+  in
+  let sigma = Evd.set_universe_context sigma uctx in
+  let body, effs = Future.force const.proof_entry_body in
+  (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+  let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+  (* EJGA: Hack related to the above call to
+     `build_constant_by_tactic` with `~opaque:Transparent`. Even if
+     the abstracted term is destined to be opaque, if we trigger the
+     `if poly && opaque && private_poly_univs ()` in `Proof_global`
+     kernel will boom. This deserves more investigation. *)
+  let const = Internal.set_opacity ~opaque const in
+  let const, args = Internal.shrink_entry sign const in
+  let cst () =
+    (* do not compute the implicit arguments, it may be costly *)
+    let () = Impargs.make_implicit_args false in
+    (* ppedrot: seems legit to have abstracted subproofs as local*)
+    declare_private_constant ~local:ImportNeedQualified ~name ~kind const
+  in
+  let cst, eff = Impargs.with_implicit_protection cst () in
+  let inst = match const.proof_entry_universes with
+  | Entries.Monomorphic_entry _ -> EConstr.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_entry_body in
+    let () = assert (Univ.ContextSet.is_empty body_uctx) in
+    EConstr.EInstance.make (Univ.UContext.instance ctx)
+  in
+  let args = List.map EConstr.of_constr args in
+  let lem = EConstr.mkConstU (cst, inst) in
+  let effs = Evd.concat_side_effects eff effs in
+  effs, sigma, lem, args, safe
+
+let get_goal_context pf i =
+  let p = get_proof pf in
+  Proof.get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = get_proof pf in
+  try Proof.get_goal_context_gen p 1
+  with
+  | Proof.NoSuchGoal _ ->
+    (* spiwack: returning empty evar_map, since if there is no goal,
+       under focus, there is no accessible evar either. EJGA: this
+       seems strange, as we have pf *)
+    let env = Global.env () in
+    Evd.from_env env, env
+
+let get_current_context pf =
+  let p = get_proof pf in
+  Proof.get_proof_context p
+
+module Proof = struct
+  type nonrec t = t
+  let get_proof = get_proof
+  let get_proof_name = get_proof_name
+  let get_used_variables = get_used_variables
+  let get_universe_decl = get_universe_decl
+  let get_initial_euctx = get_initial_euctx
+  let map_proof = map_proof
+  let map_fold_proof = map_fold_proof
+  let map_fold_proof_endline = map_fold_proof_endline
+  let set_endline_tactic = set_endline_tactic
+  let set_used_variables = set_used_variables
+  let compact = compact_the_proof
+  let update_global_env = update_global_env
+  let get_open_goals = get_open_goals
+end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 615cffeae7..1fabf80b2a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -12,14 +12,92 @@ open Names
 open Constr
 open Entries
 
-(** This module provides the official functions to declare new variables,
-   parameters, constants and inductive types. Using the following functions
-   will add the entries in the global environment (module [Global]), will
-   register the declarations in the library (module [Lib]) --- so that the
-   reset works properly --- and will fill some global tables such as
-   [Nametab] and [Impargs]. *)
-
-(** Proof entries *)
+(** This module provides the official functions to declare new
+   variables, parameters, constants and inductive types in the global
+   environment. It also updates some accesory tables such as [Nametab]
+   (name resolution), [Impargs], and [Notations]. *)
+
+(** We provide two kind of fuctions:
+
+  - one go functions, that will register a constant in one go, suited
+   for non-interactive definitions where the term is given.
+
+  - two-phase [start/declare] functions which will create an
+   interactive proof, allow its modification, and saving when
+   complete.
+
+  Internally, these functions mainly differ in that usually, the first
+  case doesn't require setting up the tactic engine.
+
+ *)
+
+(** [Declare.Proof.t] Construction of constants using interactive proofs. *)
+module Proof : sig
+
+  type t
+
+  (** XXX: These are internal and will go away from publis API once
+     lemmas is merged here *)
+  val get_proof : t -> Proof.t
+  val get_proof_name : t -> Names.Id.t
+
+  (** XXX: These 3 are only used in lemmas  *)
+  val get_used_variables : t -> Names.Id.Set.t option
+  val get_universe_decl : t -> UState.universe_decl
+  val get_initial_euctx : t -> UState.t
+
+  val map_proof : (Proof.t -> Proof.t) -> t -> t
+  val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
+  val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+
+  (** Sets the tactic to be used when a tactic line is closed with [...] *)
+  val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+
+  (** Sets the section variables assumed by the proof, returns its closure
+   * (w.r.t. type dependencies and let-ins covered by it) *)
+  val set_used_variables : t ->
+    Names.Id.t list -> Constr.named_context * t
+
+  val compact : t -> t
+
+  (** Update the proofs global environment after a side-effecting command
+      (e.g. a sublemma definition) has been run inside it. Assumes
+      there_are_pending_proofs. *)
+  val update_global_env : t -> t
+
+  val get_open_goals : t -> int
+
+end
+
+type opacity_flag = Opaque | Transparent
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion); [poly] determines if the proof is universe
+   polymorphic. The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+val start_proof
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Evd.evar_map
+  -> (Environ.env * EConstr.types) list
+  -> Proof.t
+
+(** Like [start_proof] except that there may be dependencies between
+    initial goals. *)
+val start_dependent_proof
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Proofview.telescope
+  -> Proof.t
+
+(** Proof entries represent a proof that has been finished, but still
+   not registered with the kernel.
+
+   XXX: Scheduled for removal from public API, don't rely on it *)
 type 'a proof_entry = private {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
@@ -32,12 +110,26 @@ type 'a proof_entry = private {
   proof_entry_inline_code : bool;
 }
 
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type proof_object = private
+  { name : Names.Id.t
+  (** name of the proof *)
+  ; entries : Evd.side_effects proof_entry list
+  (** list of the proof terms (in a form suitable for definitions). *)
+  ; uctx: UState.t
+  (** universe state *)
+  }
+
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
+
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
+(** XXX: Scheduled for removal from public API, don't rely on it *)
 type variable_declaration =
   | SectionLocalDef of Evd.side_effects proof_entry
   | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
 
+(** XXX: Scheduled for removal from public API, don't rely on it *)
 type 'a constant_entry =
   | DefinitionEntry of 'a proof_entry
   | ParameterEntry of parameter_entry
@@ -52,9 +144,9 @@ val declare_variable
   -> unit
 
 (** Declaration of global constructions
-   i.e. Definition/Theorem/Axiom/Parameter/... *)
+   i.e. Definition/Theorem/Axiom/Parameter/...
 
-(* Default definition entries, transparent with no secctx or proj information *)
+   XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
 val definition_entry
   : ?fix_exn:Future.fix_exn
   -> ?opaque:bool
@@ -70,6 +162,7 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
+(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
 val pure_definition_entry
   : ?fix_exn:Future.fix_exn
   -> ?opaque:bool
@@ -79,17 +172,6 @@ val pure_definition_entry
   -> constr
   -> unit proof_entry
 
-(* Delayed definition entries *)
-val delayed_definition_entry
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> ?feedback_id:Stateid.t
-  -> ?section_vars:Id.Set.t
-  -> ?univs:Entries.universes_entry
-  -> ?types:types
-  -> 'a Entries.const_entry_body
-  -> 'a proof_entry
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** [declare_constant id cd] declares a global declaration
@@ -97,7 +179,9 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
    the full path of the declaration
 
   internal specify if the constant has been created by the kernel or by the
-  user, and in the former case, if its errors should be silent *)
+  user, and in the former case, if its errors should be silent
+
+  XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
 val declare_constant
   :  ?local:import_status
   -> name:Id.t
@@ -115,7 +199,9 @@ val declare_private_constant
 
 (** [inline_private_constants ~sideff ~uctx env ce] will inline the
    constants in [ce]'s body and return the body plus the updated
-   [UState.t]. *)
+   [UState.t].
+
+   XXX: Scheduled for removal from public API, don't rely on it *)
 val inline_private_constants
   :  uctx:UState.t
   -> Environ.env
@@ -124,10 +210,10 @@ val inline_private_constants
 
 (** Declaration messages *)
 
+(** XXX: Scheduled for removal from public API, do not use *)
 val definition_message : Id.t -> unit
 val assumption_message : Id.t -> unit
 val fixpoint_message : int array option -> Id.t list -> unit
-val cofixpoint_message : Id.t list -> unit
 val recursive_message : bool (** true = fixpoint *) ->
   int array option -> Id.t list -> unit
 
@@ -157,3 +243,72 @@ module Internal : sig
   val objVariable : unit Libobject.Dyn.tag
 
 end
+
+(* Intermediate step necessary to delegate the future.
+ * Both access the current proof state. The former is supposed to be
+ * chained with a computation that completed the proof *)
+type closed_proof_output
+
+(** Requires a complete proof. *)
+val return_proof : Proof.t -> closed_proof_output
+
+(** An incomplete proof is allowed (no error), and a warn is given if
+   the proof is complete. *)
+val return_partial_proof : Proof.t -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
+
+(** [by tac] applies tactic [tac] to the 1st subgoal of the current
+    focused proof.
+    Returns [false] if an unsafe tactic has been used. *)
+val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
+
+(** Declare abstract constant; will check no evars are possible; *)
+val declare_abstract :
+     name:Names.Id.t
+  -> poly:bool
+  -> kind:Decls.logical_kind
+  -> sign:EConstr.named_context
+  -> secsign:Environ.named_context_val
+  -> opaque:bool
+  -> solve_tac:unit Proofview.tactic
+  -> Evd.evar_map
+  -> EConstr.t
+  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool
+
+val build_by_tactic
+  :  ?side_eff:bool
+  -> Environ.env
+  -> uctx:UState.t
+  -> poly:bool
+  -> typ:EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Constr.types option * bool * UState.t
+
+(** {6 Helpers to obtain proof state when in an interactive proof } *)
+
+(** [get_goal_context n] returns the context of the [n]th subgoal of
+   the current focused proof or raises a [UserError] if there is no
+   focused proof or if there is no more subgoals *)
+
+val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
+
+(** [get_current_context ()] returns the context of the
+  current focused goal. If there is no focused goal but there
+  is a proof in progress, it returns the corresponding evar_map.
+  If there is no pending proof then it returns the current global
+  environment and empty evar_map. *)
+val get_current_context : Proof.t -> Evd.evar_map * Environ.env
+
+(** Temporarily re-exported for 3rd party code; don't use  *)
+val build_constant_by_tactic :
+  name:Names.Id.t ->
+  ?opaque:opacity_flag ->
+  uctx:UState.t ->
+  sign:Environ.named_context_val ->
+  poly:bool ->
+  EConstr.types ->
+  unit Proofview.tactic ->
+  Evd.side_effects proof_entry * bool * UState.t
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2118b4f231..ffb0e030db 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1562,7 +1562,7 @@ let pr_hint_term env sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Proof_global.get_proof pf in
+  let pts = Declare.Proof.get_proof pf in
   let Proof.{goals;sigma} = Proof.data pts in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9e11931247..eed0e37fac 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -306,7 +306,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Proof_global.t -> Pp.t
+val pr_applicable_hint : Declare.Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
deleted file mode 100644
index c139594f13..0000000000
--- a/tactics/pfedit.ml
+++ /dev/null
@@ -1,189 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-open Environ
-open Evd
-
-let use_unification_heuristics =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Solve";"Unification";"Constraints"]
-    ~value:true
-
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Some Pp.(str "No such goal.")
-  | _ -> None
-end
-
-let get_nth_V82_goal p i =
-  let Proof.{ sigma; goals } = Proof.data p in
-  try { it = List.nth goals (i-1) ; sigma }
-  with Failure _ -> raise NoSuchGoal
-
-let get_goal_context_gen pf i =
-  let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
-  (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-
-let get_goal_context pf i =
-  let p = Proof_global.get_proof pf in
-  get_goal_context_gen p i
-
-let get_current_goal_context pf =
-  let p = Proof_global.get_proof pf in
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* spiwack: returning empty evar_map, since if there is no goal,
-       under focus, there is no accessible evar either. EJGA: this
-       seems strange, as we have pf *)
-    let env = Global.env () in
-    Evd.from_env env, env
-
-let get_proof_context p =
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* No more focused goals *)
-    let { Proof.sigma } = Proof.data p in
-    sigma, Global.env ()
-
-let get_current_context pf =
-  let p = Proof_global.get_proof pf in
-  get_proof_context p
-
-let solve ?with_end_tac gi info_lvl tac pr =
-    let tac = match with_end_tac with
-      | None -> tac
-      | Some etac -> Proofview.tclTHEN tac etac in
-    let tac = match info_lvl with
-      | None -> tac
-      | Some _ -> Proofview.Trace.record_info_trace tac
-    in
-    let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
-    let tac = let open Goal_select in match gi with
-      | SelectAlreadyFocused ->
-        let open Proofview.Notations in
-        Proofview.numgoals >>= fun n ->
-        if n == 1 then tac
-        else
-          let e = CErrors.UserError
-              (None,
-               Pp.(str "Expected a single focused goal but " ++
-                   int n ++ str " goals are focused."))
-          in
-          Proofview.tclZERO e
-
-      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
-      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
-      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
-      | SelectAll -> tac
-    in
-    let tac =
-      if use_unification_heuristics () then
-        Proofview.tclTHEN tac Refine.solve_constraints
-      else tac
-    in
-    let env = Global.env () in
-    let (p,(status,info),()) = Proof.run_tactic env tac pr in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let () =
-      match info_lvl with
-      | None -> ()
-      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
-    in
-    (p,status)
-
-let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac)
-
-(**********************************************************************)
-(* Shortcut to build a term using tactics *)
-
-let next = let n = ref 0 in fun () -> incr n; !n
-
-let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac =
-  let evd = Evd.from_ctx uctx in
-  let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
-  let pf, status = by tac pf in
-  let open Proof_global in
-  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
-  match entries with
-  | [entry] ->
-    entry, status, uctx
-  | _ ->
-    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-
-let build_by_tactic ?(side_eff=true) env ~uctx ~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 ~uctx ~sign ~poly typ tac in
-  let cb, uctx =
-    if side_eff then Declare.inline_private_constants ~uctx env ce
-    else
-      (* GG: side effects won't get reset: no need to treat their universes specially *)
-      let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in
-      cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
-  in
-  cb, ce.Declare.proof_entry_type, status, univs
-
-let refine_by_tactic ~name ~poly env sigma ty tac =
-  (* Save the initial side-effects to restore them afterwards. We set the
-     current set of side-effects to be empty so that we can retrieve the
-     ones created during the tactic invocation easily. *)
-  let eff = Evd.eval_side_effects sigma in
-  let sigma = Evd.drop_side_effects sigma in
-  (* Save the existing goals *)
-  let prev_future_goals = save_future_goals sigma in
-  (* Start a proof *)
-  let prf = Proof.start ~name ~poly sigma [env, ty] in
-  let (prf, _, ()) =
-    try Proof.run_tactic env tac prf
-    with Logic_monad.TacticFailure e as src ->
-      (* Catch the inner error of the monad tactic *)
-      let (_, info) = Exninfo.capture src in
-      Exninfo.iraise (e, info)
-  in
-  (* Plug back the retrieved sigma *)
-  let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
-  assert (stack = []);
-  let ans = match Proofview.initial_goals entry with
-  | [c, _] -> c
-  | _ -> assert false
-  in
-  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
-  (* [neff] contains the freshly generated side-effects *)
-  let neff = Evd.eval_side_effects sigma in
-  (* Reset the old side-effects *)
-  let sigma = Evd.drop_side_effects sigma in
-  let sigma = Evd.emit_side_effects eff sigma in
-  (* Restore former goals *)
-  let sigma = restore_future_goals sigma prev_future_goals in
-  (* Push remaining goals as future_goals which is the only way we
-     have to inform the caller that there are goals to collect while
-     not being encapsulated in the monad *)
-  (* Goals produced by tactic "shelve" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
-  (* Goals produced by tactic "give_up" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
-  (* Other goals *)
-  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
-  (* Get rid of the fresh side-effects by internalizing them in the term
-     itself. Note that this is unsound, because the tactic may have solved
-     other goals that were already present during its invocation, so that
-     those goals rely on effects that are not present anymore. Hopefully,
-     this hack will work in most cases. *)
-  let neff = neff.Evd.seff_private in
-  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
-  ans, sigma
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
deleted file mode 100644
index c49e997757..0000000000
--- a/tactics/pfedit.mli
+++ /dev/null
@@ -1,94 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
-
-open Names
-open Constr
-open Environ
-
-(** {6 ... } *)
-
-exception NoSuchGoal
-
-(** [get_goal_context n] returns the context of the [n]th subgoal of
-   the current focused proof or raises a [UserError] if there is no
-   focused proof or if there is no more subgoals *)
-
-val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
-
-(** [get_current_goal_context ()] works as [get_goal_context 1] *)
-val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
-
-(** [get_proof_context ()] gets the goal context for the first subgoal
-    of the proof *)
-val get_proof_context : Proof.t -> Evd.evar_map * env
-
-(** [get_current_context ()] returns the context of the
-  current focused goal. If there is no focused goal but there
-  is a proof in progress, it returns the corresponding evar_map.
-  If there is no pending proof then it returns the current global
-  environment and empty evar_map. *)
-val get_current_context : Proof_global.t -> Evd.evar_map * env
-
-(** {6 ... } *)
-
-(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
-    subgoal of the current focused proof. [solve SelectAll
-    tac] applies [tac] to all subgoals. *)
-
-val solve : ?with_end_tac:unit Proofview.tactic ->
-      Goal_select.t -> int option -> unit Proofview.tactic ->
-      Proof.t -> Proof.t * bool
-
-(** [by tac] applies tactic [tac] to the 1st subgoal of the current
-    focused proof.
-    Returns [false] if an unsafe tactic has been used. *)
-
-val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
-
-(** Option telling if unification heuristics should be used. *)
-val use_unification_heuristics : unit -> bool
-
-(** [build_by_tactic typ tac] returns a term of type [typ] by calling
-    [tac]. The return boolean, if [false] indicates the use of an unsafe
-    tactic. *)
-
-val build_constant_by_tactic
-  :  name:Id.t
-  -> ?opaque:Proof_global.opacity_flag
-  -> uctx:UState.t
-  -> sign:named_context_val
-  -> poly:bool
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> Evd.side_effects Declare.proof_entry * bool * UState.t
-
-val build_by_tactic
-  :  ?side_eff:bool
-  -> env
-  -> uctx:UState.t
-  -> poly:bool
-  -> typ:EConstr.types
-  -> unit Proofview.tactic
-  -> constr * types option * bool * UState.t
-
-val refine_by_tactic
-  :  name:Id.t
-  -> poly:bool
-  -> env -> Evd.evar_map
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> constr * Evd.evar_map
-(** A variant of the above function that handles open terms as well.
-    Caveat: all effects are purged in the returned term at the end, but other
-    evars solved by side-effects are NOT purged, so that unexpected failures may
-    occur. Ideally all code using this function should be rewritten in the
-    monad. *)
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
deleted file mode 100644
index 98de0c848b..0000000000
--- a/tactics/proof_global.ml
+++ /dev/null
@@ -1,284 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Names
-open Context
-
-module NamedDecl = Context.Named.Declaration
-
-(*** Proof Global Environment ***)
-
-type proof_object =
-  { name : Names.Id.t
-  (* [name] only used in the STM *)
-  ; entries : Evd.side_effects Declare.proof_entry list
-  ; uctx: UState.t
-  }
-
-type opacity_flag = Opaque | Transparent
-
-type t =
-  { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Id.Set.t option
-  ; proof : Proof.t
-  ; udecl: UState.universe_decl
-  (** Initial universe declarations *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
-  }
-
-(*** Proof Global manipulation ***)
-
-let get_proof ps = ps.proof
-let get_proof_name ps = (Proof.data ps.proof).Proof.name
-
-let get_initial_euctx ps = ps.initial_euctx
-
-let map_proof f p = { p with proof = f p.proof }
-let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
-
-let map_fold_proof_endline f ps =
-  let et =
-    match ps.endline_tactic with
-    | None -> Proofview.tclUNIT ()
-    | Some tac ->
-      let open Geninterp in
-      let {Proof.poly} = Proof.data ps.proof in
-      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
-      let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
-      let tac = Geninterp.interp tag ist tac in
-      Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
-  in
-  let (newpr,ret) = f et ps.proof in
-  let ps = { ps with proof = newpr } in
-  ps, ret
-
-let compact_the_proof pf = map_proof Proof.compact pf
-
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac ps =
-  { ps with endline_tactic = Some tac }
-
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
-   name [name] with goals [goals] (a list of pairs of environment and
-   conclusion). The proof is started in the evar map [sigma] (which
-   can typically contain universe constraints), and with universe
-   bindings [udecl]. *)
-let start_proof ~name ~udecl ~poly sigma goals =
-  let proof = Proof.start ~name ~poly sigma goals in
-  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
-  { proof
-  ; endline_tactic = None
-  ; section_vars = None
-  ; udecl
-  ; initial_euctx
-  }
-
-let start_dependent_proof ~name ~udecl ~poly goals =
-  let proof = Proof.dependent_start ~name ~poly goals in
-  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
-  { proof
-  ; endline_tactic = None
-  ; section_vars = None
-  ; udecl
-  ; initial_euctx
-  }
-
-let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.udecl
-
-let set_used_variables ps l =
-  let open Context.Named.Declaration in
-  let env = Global.env () in
-  let ids = List.fold_right Id.Set.add l Id.Set.empty in
-  let ctx = Environ.keep_hyps env ids in
-  let ctx_set =
-    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
-  let vars_of = Environ.global_vars_set in
-  let aux env entry (ctx, all_safe as orig) =
-    match entry with
-    | LocalAssum ({binder_name=x},_) ->
-       if Id.Set.mem x all_safe then orig
-       else (ctx, all_safe)
-    | LocalDef ({binder_name=x},bo, ty) as decl ->
-       if Id.Set.mem x all_safe then orig else
-       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
-       if Id.Set.subset vars all_safe
-       then (decl :: ctx, Id.Set.add x all_safe)
-       else (ctx, all_safe) in
-  let ctx, _ =
-    Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
-  if not (Option.is_empty ps.section_vars) then
-    CErrors.user_err Pp.(str "Used section variables can be declared only once");
-  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
-
-let get_open_goals ps =
-  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
-  List.length goals +
-  List.fold_left (+) 0
-    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
-  List.length shelf
-
-type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
-
-let private_poly_univs =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Private";"Polymorphic";"Universes"]
-    ~value:true
-
-(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
-(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
-let prepare_proof ~unsafe_typ { proof } =
-  let Proof.{name=pid;entry;poly} = Proof.data proof in
-  let initial_goals = Proofview.initial_goals entry in
-  let evd = Proof.return ~pid proof in
-  let eff = Evd.eval_side_effects evd in
-  let evd = Evd.minimize_universes evd in
-  let to_constr_body c =
-    match EConstr.to_constr_opt evd c with
-    | Some p -> p
-    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
-  in
-  let to_constr_typ t =
-    if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
-  in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
-  (* EJGA: actually side-effects de-duplication and this codepath is
-     unrelated. Duplicated side-effects arise from incorrect scheme
-     generation code, the main bulk of it was mostly fixed by #9836
-     but duplication can still happen because of rewriting schemes I
-     think; however the code below is mostly untested, the only
-     code-paths that generate several proof entries are derive and
-     equations and so far there is no code in the CI that will
-     actually call those and do a side-effect, TTBOMK *)
-  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
-  let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
-  proofs, Evd.evar_universe_context evd
-
-let close_proof ~opaque ~keep_body_ucst_separate ps =
-
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly } = Proof.data proof in
-  let unsafe_typ = keep_body_ucst_separate && not poly in
-  let elist, uctx = prepare_proof ~unsafe_typ ps in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
-
-  let make_entry ((body, eff), typ) =
-
-    let allow_deferred =
-      not poly &&
-      (keep_body_ucst_separate
-       || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
-    in
-    let used_univs_body = Vars.universes_of_constr body in
-    let used_univs_typ = Vars.universes_of_constr typ in
-    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-    let utyp, ubody =
-      if allow_deferred then
-        let utyp = UState.univ_entry ~poly initial_euctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-        (* For vi2vo compilation proofs are computed now but we need to
-           complement the univ constraints of the typ with the ones of
-           the body.  So we keep the two sets distinct. *)
-        let uctx_body = UState.restrict uctx used_univs in
-        let ubody = UState.check_mono_univ_decl uctx_body udecl in
-        utyp, ubody
-      else if poly && opaque && private_poly_univs () then
-        let universes = UState.restrict uctx used_univs in
-        let typus = UState.restrict universes used_univs_typ in
-        let utyp = UState.check_univ_decl ~poly typus udecl in
-        let ubody = Univ.ContextSet.diff
-            (UState.context_set universes)
-            (UState.context_set typus)
-        in
-        utyp, ubody
-      else
-        (* Since the proof is computed now, we can simply have 1 set of
-           constraints in which we merge the ones for the body and the ones
-           for the typ. We recheck the declaration after restricting with
-           the actually used universes.
-           TODO: check if restrict is really necessary now. *)
-        let ctx = UState.restrict uctx used_univs in
-        let utyp = UState.check_univ_decl ~poly ctx udecl in
-        utyp, Univ.ContextSet.empty
-    in
-    Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
-  in
-  let entries = CList.map make_entry elist  in
-  { name; entries; uctx }
-
-let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let { Proof.name; poly; entry; sigma } = Proof.data proof in
-
-  (* We don't allow poly = true in this path *)
-  if poly then
-    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
-
-  let fpl, uctx = Future.split2 fpl in
-  (* Because of dependent subgoals at the beginning of proofs, we could
-     have existential variables in the initial types of goals, we need to
-     normalise them for the kernel. *)
-  let subst_evar k = Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
-
-  (* We only support opaque proofs, this will be enforced by using
-     different entries soon *)
-  let opaque = true in
-  let make_entry p (_, types) =
-    (* Already checked the univ_decl for the type universes when starting the proof. *)
-    let univs = UState.univ_entry ~poly:false initial_euctx in
-    let types = nf (EConstr.Unsafe.to_constr types) in
-
-    Future.chain p (fun (pt,eff) ->
-        (* Deferred proof, we already checked the universe declaration with
-             the initial universes, ensure that the final universes respect
-             the declaration as well. If the declaration is non-extensible,
-             this will prevent the body from adding universes and constraints. *)
-        let uctx = Future.force uctx in
-        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
-        let used_univs = Univ.LSet.union
-            (Vars.universes_of_constr types)
-            (Vars.universes_of_constr pt)
-        in
-        let univs = UState.restrict uctx used_univs in
-        let univs = UState.check_mono_univ_decl univs udecl in
-        (pt,univs),eff)
-    |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types
-  in
-  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx }
-
-let close_future_proof = close_proof_delayed
-
-let return_partial_proof { proof } =
- let proofs = Proof.partial_proof proof in
- let Proof.{sigma=evd} = Proof.data proof in
- let eff = Evd.eval_side_effects evd in
- (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
- let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
- proofs, Evd.evar_universe_context evd
-
-let return_proof ps =
-  let p, uctx = prepare_proof ~unsafe_typ:false ps in
-  List.map fst p, uctx
-
-let update_global_env =
-  map_proof (fun p ->
-      let { Proof.sigma } = Proof.data p in
-      let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-      let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
-      p)
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
deleted file mode 100644
index 874708ded8..0000000000
--- a/tactics/proof_global.mli
+++ /dev/null
@@ -1,98 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** State for interactive proofs. *)
-
-type t
-
-(* Should be moved into a proper view *)
-val get_proof : t -> Proof.t
-val get_proof_name : t -> Names.Id.t
-val get_used_variables : t -> Names.Id.Set.t option
-
-(** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : t -> UState.universe_decl
-
-(** Get initial universe state *)
-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] *)
-type proof_object =
-  { name : Names.Id.t
-  (** name of the proof *)
-  ; entries : Evd.side_effects Declare.proof_entry list
-  (** list of the proof terms (in a form suitable for definitions). *)
-  ; uctx: UState.t
-  (** universe state *)
-  }
-
-type opacity_flag = Opaque | Transparent
-
-(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
-   name [name] with goals [goals] (a list of pairs of environment and
-   conclusion); [poly] determines if the proof is universe
-   polymorphic. The proof is started in the evar map [sigma] (which
-   can typically contain universe constraints), and with universe
-   bindings [udecl]. *)
-val start_proof
-  :  name:Names.Id.t
-  -> udecl:UState.universe_decl
-  -> poly:bool
-  -> Evd.evar_map
-  -> (Environ.env * EConstr.types) list
-  -> t
-
-(** Like [start_proof] except that there may be dependencies between
-    initial goals. *)
-val start_dependent_proof
-  :  name:Names.Id.t
-  -> udecl:UState.universe_decl
-  -> poly:bool
-  -> Proofview.telescope
-  -> t
-
-(** Update the proofs global environment after a side-effecting command
-  (e.g. a sublemma definition) has been run inside it. Assumes
-  there_are_pending_proofs. *)
-val update_global_env : t -> t
-
-(* Takes a function to add to the exceptions data relative to the
-   state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
-
-(* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The former is supposed to be
- * chained with a computation that completed the proof *)
-
-type closed_proof_output
-
-(** Requires a complete proof. *)
-val return_proof : t -> closed_proof_output
-
-(** An incomplete proof is allowed (no error), and a warn is given if
-   the proof is complete. *)
-val return_partial_proof : t -> closed_proof_output
-val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
-
-val get_open_goals : t -> int
-
-val map_proof : (Proof.t -> Proof.t) -> t -> t
-val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
-val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
-
-(** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
-
-(** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies and let-ins covered by it) *)
-val set_used_variables : t ->
-  Names.Id.t list -> Constr.named_context * t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0c4e496650..537d111f23 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,7 +1,5 @@
 DeclareScheme
 Declare
-Proof_global
-Pfedit
 Dnet
 Dn
 Btermdn
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 9d8e830d64..593d0c7f67 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -136,7 +136,7 @@ h': newdef n <> n
 (use "About" for full details on implicit arguments)
 (use "About" for full details on implicit arguments)
 The command has indeed failed with message:
-No such goal.
+[Focus] No such goal.
 The command has indeed failed with message:
 Query commands only support the single numbered goal selector.
 The command has indeed failed with message:
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index a7a9b77b56..c8b8660b92 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -131,7 +131,7 @@ let set_options = List.iter set_option
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
   let check_pending_proofs () =
-    let pfs = Vernacstate.Proof_global.get_all_proof_names () [@ocaml.warning "-3"] in
+    let pfs = Vernacstate.Declare.get_all_proof_names () [@ocaml.warning "-3"] in
     if not (CList.is_empty pfs) then
       fatal_error (str "There are pending proofs: "
                     ++ (pfs
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b8acdd3af1..2c5faa4df7 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -191,8 +191,8 @@ end
     from cycling. *)
 let make_prompt () =
   try
-    (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ())) ^ " < "
-  with Vernacstate.Proof_global.NoCurrentProof ->
+    (Names.Id.to_string (Vernacstate.Declare.get_current_proof_name ())) ^ " < "
+  with Vernacstate.Declare.NoCurrentProof ->
     "Coq < "
   [@@ocaml.warning "-3"]
 
@@ -352,7 +352,7 @@ let print_anyway c =
 let top_goal_print ~doc c oldp newp =
   try
     let proof_changed = not (Option.equal cproof oldp newp) in
-    let print_goals = proof_changed && Vernacstate.Proof_global.there_are_pending_proofs () ||
+    let print_goals = proof_changed && Vernacstate.Declare.there_are_pending_proofs () ||
                       print_anyway c in
     if not !Flags.quiet && print_goals then begin
       let dproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
@@ -375,7 +375,7 @@ let exit_on_error =
    point we should consolidate the code *)
 let show_proof_diff_to_pp pstate =
   let p = Option.get pstate in
-  let sigma, env = Pfedit.get_proof_context p in
+  let sigma, env = Proof.get_proof_context p in
   let pprf = Proof.partial_proof p in
   Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
 
@@ -392,7 +392,7 @@ let show_proof_diff_cmd ~state removed =
         let show_removed = Some removed in
         Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
       with
-      | Pfedit.NoSuchGoal
+      | Proof.NoSuchGoal _
       | Option.IsNone -> n_pp
       | Pp_diff.Diff_Failure msg -> begin
           (* todo: print the unparsable string (if we know it) *)
@@ -403,7 +403,7 @@ let show_proof_diff_cmd ~state removed =
     else
       n_pp
   with
-  | Pfedit.NoSuchGoal
+  | Proof.NoSuchGoal _
   | Option.IsNone ->
     CErrors.user_err (str "No goals to show.")
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 076796468f..c4c8492a4a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -66,7 +66,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
 
       (* Force the command  *)
       let ndoc = if check then Stm.observe ~doc nsid else doc in
-      let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in
+      let new_proof = Vernacstate.Declare.give_me_the_proof_opt () [@ocaml.warning "-3"] in
       { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
       let (reraise, info) = Exninfo.capture reraise in
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 72df4d75c8..2102cd1172 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1290,7 +1290,7 @@ let () =
     let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
-    let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
+    let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 3e920fcc2d..28e877491e 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -795,7 +795,7 @@ let perform_eval ~pstate e =
       Goal_select.SelectAll, Proof.start ~name ~poly sigma []
     | Some pstate ->
       Goal_select.get_default_goal_selector (),
-      Proof_global.get_proof pstate
+      Declare.Proof.get_proof pstate
   in
   let v = match selector with
   | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
@@ -899,10 +899,10 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Proof_global.map_fold_proof_endline begin fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_proof_endline begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
-    let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
+    let (p, status) = Proof.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index edad118dc9..fc56a54e3a 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -31,7 +31,7 @@ val register_struct
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
-val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
+val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit
 
 (** {5 Notations} *)
 
@@ -53,7 +53,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
+val call : pstate:Declare.Proof.t -> default:bool -> raw_tacexpr -> Declare.Proof.t
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f3ad324aa5..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) = Pfedit.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) = Pfedit.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) = Pfedit.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 7f7340bb34..b13e5bf653 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.Proof.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.Proof.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 = Pfedit.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.Proof.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.Proof.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.Proof.get_universe_decl lemma.proof in
+  let Proof.{ poly; entry } = Proof.data (Declare.Proof.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.Proof.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.Proof.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..bd2e87ac3a 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.Proof.t -> Declare.Proof.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.Proof.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 435085793c..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 =
-      Pfedit.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/pfedit.ml b/vernac/pfedit.ml
new file mode 100644
index 0000000000..d6b9592176
--- /dev/null
+++ b/vernac/pfedit.ml
@@ -0,0 +1,9 @@
+(* Compat API / *)
+let get_current_context = Declare.get_current_context
+let solve = Proof.solve
+let by = Declare.by
+let refine_by_tactic = Proof.refine_by_tactic
+
+(* We don't want to export this anymore, but we do for now *)
+let build_by_tactic = Declare.build_by_tactic
+let build_constant_by_tactic = Declare.build_constant_by_tactic
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/proof_global.ml b/vernac/proof_global.ml
new file mode 100644
index 0000000000..b6c07042e2
--- /dev/null
+++ b/vernac/proof_global.ml
@@ -0,0 +1,7 @@
+(* compatibility module; can be removed once we agree on the API *)
+
+type t = Declare.Proof.t
+let map_proof = Declare.Proof.map_proof
+let get_proof = Declare.Proof.get_proof
+
+type opacity_flag = Declare.opacity_flag = Opaque | Transparent
diff --git a/vernac/search.ml b/vernac/search.ml
index 68a30b4231..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 -> Pfedit.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..d3b8444b5f 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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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/vernac.mllib b/vernac/vernac.mllib
index 5a2bdb43d4..b7728fe699 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -44,3 +44,5 @@ ComArguments
 Vernacentries
 Vernacstate
 Vernacinterp
+Proof_global
+Pfedit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6de14997d4..044e479aeb 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 -> Pfedit.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 -> Pfedit.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 = Pfedit.get_current_context pstate in
+    let p = Declare.Proof.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
-  | Pfedit.NoSuchGoal
+  | Proof.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 =
-        Pfedit.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.Proof.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.Proof.set_endline_tactic tac pstate
 
-let vernac_set_used_variables ~pstate e : Proof_global.t =
+let vernac_set_used_variables ~pstate e : Declare.Proof.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.Proof.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.Proof.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 -> Pfedit.get_goal_context lemma n
-    | None -> Pfedit.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.Proof.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 = Pfedit.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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.Proof.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..d772f274a2 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.Proof.t -> Declare.Proof.t)
+  | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
+  | VtReadProof of (pstate:Declare.Proof.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d0ebc1086..58c267080a 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.Proof.t -> Declare.Proof.t)
+  | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
+  | VtReadProof of (pstate:Declare.Proof.t -> unit)
 
 type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index eb299222dd..19d41c4770 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.Proof.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 a4e9c8e1ab..0fca1e9078 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.Proof.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
@@ -145,23 +145,23 @@ module Proof_global = struct
     | Some x -> s_lemmas := Some (LemmaStack.map_top_pstate ~f x)
 
   let there_are_pending_proofs () = !s_lemmas <> None
-  let get_open_goals () = cc get_open_goals
+  let get_open_goals () = cc Proof.get_open_goals
 
-  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:get_proof) !s_lemmas
-  let give_me_the_proof () = cc get_proof
-  let get_current_proof_name () = cc get_proof_name
+  let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:Proof.get_proof) !s_lemmas
+  let give_me_the_proof () = cc Proof.get_proof
+  let get_current_proof_name () = cc Proof.get_proof_name
 
-  let map_proof f = dd (map_proof f)
+  let map_proof f = dd (Proof.map_proof f)
   let with_current_proof f =
     match !s_lemmas with
     | None -> raise NoCurrentProof
     | Some stack ->
-      let pf, res = LemmaStack.with_top_pstate stack ~f:(map_fold_proof_endline f) in
+      let pf, res = LemmaStack.with_top_pstate stack ~f:(Proof.map_fold_proof_endline f) in
       let stack = LemmaStack.map_top_pstate stack ~f:(fun _ -> pf) in
       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 update_global_env () = dd (Proof.update_global_env)
 
-  let get_current_context () = cc Pfedit.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..fb6d8b6db6 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.Proof.t -> Declare.Proof.t) -> t -> t
+  val with_top_pstate : t -> f:(Declare.Proof.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.Proof.t option
 
   val freeze : marshallable:bool -> LemmaStack.t option
   val unfreeze : LemmaStack.t -> unit