[declare] Move proof_entry type to declare, put interactive proof data on top of declare.

This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.

This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.

This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.

A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.

Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.

5 files changed, 0 insertions, 721 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
deleted file mode 100644
index 99a254652c..0000000000
--- a/proofs/pfedit.ml
+++ /dev/null
@@ -1,195 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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_ref = ref true
-let () = Goptions.(declare_bool_option {
-  optdepr = false;
-  optname = "Solve unification constraints at every \".\"";
-  optkey = ["Solve";"Unification";"Constraints"];
-  optread = (fun () -> !use_unification_heuristics_ref);
-  optwrite = (fun a -> use_unification_heuristics_ref:=a);
-})
-
-let use_unification_heuristics () = !use_unification_heuristics_ref
-
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
-  | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
-  | _ -> raise CErrors.Unhandled
-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_current_context pf =
-  let p = Proof_global.get_proof pf in
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* No more focused goals *)
-    let { Proof.sigma } = Proof.data p in
-    sigma, Global.env ()
-
-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 ctx sign ~poly typ tac =
-  let evd = Evd.from_ctx ctx 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
-  try
-    let pf, status = by tac pf in
-    let open Proof_global in
-    let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
-    match entries with
-    | [entry] ->
-      let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in
-      entry, status, univs
-    | _ ->
-      CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    iraise reraise
-
-let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
-  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = val_of_named_context (named_context env) in
-  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
-  let body, eff = Future.force ce.Proof_global.proof_entry_body in
-  let (cb, ctx) =
-    if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
-    else body
-  in
-  let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
-  cb, 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) = CErrors.push src in
-      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/proofs/pfedit.mli b/proofs/pfedit.mli
deleted file mode 100644
index 0626e40047..0000000000
--- a/proofs/pfedit.mli
+++ /dev/null
@@ -1,89 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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_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
-  -> UState.t
-  -> named_context_val
-  -> poly:bool
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
-
-val build_by_tactic
-  :  ?side_eff:bool
-  -> env
-  -> UState.t
-  -> poly:bool
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> constr * 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/proofs/proof_global.ml b/proofs/proof_global.ml
deleted file mode 100644
index 851a3d1135..0000000000
--- a/proofs/proof_global.ml
+++ /dev/null
@@ -1,314 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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)         *)
-(************************************************************************)
-
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines proof facilities relevant to the           *)
-(*      toplevel. In particular it defines the global proof            *)
-(*      environment.                                                   *)
-(*                                                                     *)
-(***********************************************************************)
-
-open Util
-open Names
-open Context
-
-module NamedDecl = Context.Named.Declaration
-
-(*** Proof Global Environment ***)
-
-type 'a proof_entry = {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
-  (* State id on which the completion of type checking is reported *)
-  proof_entry_feedback : Stateid.t option;
-  proof_entry_type        : Constr.types option;
-  proof_entry_universes   : Entries.universes_entry;
-  proof_entry_opaque      : bool;
-  proof_entry_inline_code : bool;
-}
-
-type proof_object =
-  { name : Names.Id.t
-  ; entries : Evd.side_effects proof_entry list
-  ; poly : bool
-  ; universes: UState.t
-  ; udecl : UState.universe_decl
-  }
-
-type opacity_flag = Opaque | Transparent
-
-type t =
-  { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Constr.named_context 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");
-  (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), { ps with section_vars = Some 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 =
-  let b = ref true in
-  let _ = Goptions.(declare_bool_option {
-      optdepr = false;
-      optname = "use private polymorphic universes for Qed constants";
-      optkey = ["Private";"Polymorphic";"Universes"];
-      optread = (fun () -> !b);
-      optwrite = ((:=) b);
-    })
-  in
-  fun () -> !b
-
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
-                (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let Proof.{ name; poly; entry } = Proof.data proof in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
-  let constrain_variables ctx =
-    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
-  in
-  let fpl, univs = Future.split2 fpl in
-  let universes = if poly || now then Future.force univs else initial_euctx 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 =
-    let { Proof.sigma } = Proof.data proof in
-    Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
-    (UState.subst universes) in
-
-  let make_body =
-    if poly || now then
-      let make_body t (c, eff) =
-        let body = c in
-        let allow_deferred =
-          not poly && (keep_body_ucst_separate ||
-          not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
-        in
-        let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Vars.universes_of_constr body in
-        let used_univs_typ = Vars.universes_of_constr typ in
-        if allow_deferred then
-          let initunivs = UState.univ_entry ~poly initial_euctx in
-          let ctx = constrain_variables universes 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body udecl in
-          (initunivs, typ), ((body, univs), eff)
-        else if poly && opaque && private_poly_univs () then
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let universes = UState.restrict universes used_univs in
-          let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus udecl in
-          let ubody = Univ.ContextSet.diff
-              (UState.context_set universes)
-              (UState.context_set typus)
-          in
-          (udecl, typ), ((body, ubody), eff)
-        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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = UState.restrict universes used_univs in
-          let univs = UState.check_univ_decl ~poly ctx udecl in
-          (univs, typ), ((body, Univ.ContextSet.empty), eff)
-      in 
-       fun t p -> Future.split2 (Future.chain p (make_body t))
-    else
-      fun t p ->
-        (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = UState.univ_entry ~poly:false universes in
-        let t = nf t in
-        Future.from_val (univctx, t),
-        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 univs = Future.force univs in
-          let univs = constrain_variables univs in
-          let used_univs = Univ.LSet.union
-              (Vars.universes_of_constr t)
-              (Vars.universes_of_constr pt)
-          in
-          let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs udecl in
-          (pt,univs),eff)
-  in
-  let entry_fn p (_, t) =
-    let t = EConstr.Unsafe.to_constr t in
-    let univstyp, body = make_body t p in
-    let univs, typ = Future.force univstyp in
-    {
-      proof_entry_body = body;
-      proof_entry_secctx = section_vars;
-      proof_entry_feedback = feedback_id;
-      proof_entry_type  = Some typ;
-      proof_entry_inline_code = false;
-      proof_entry_opaque = opaque;
-      proof_entry_universes = univs; }
-  in
-  let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { name; entries = entries; poly; universes; udecl }
-
-let return_proof ?(allow_partial=false) ps =
- let { proof } = ps in
- if allow_partial then begin
-  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
- end else
-  let Proof.{name=pid;entry} = 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 proof_opt c =
-    match EConstr.to_constr_opt evd c with
-    | Some p -> p
-    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
-  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 *)
-  let proofs =
-    List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
-    proofs, Evd.evar_universe_context evd
-
-let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
-
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
-  close_proof ~opaque ~keep_body_ucst_separate ~now:true
-    (Future.from_val ~fix_exn (return_proof ps)) ps
-
-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/proofs/proof_global.mli b/proofs/proof_global.mli
deleted file mode 100644
index 54d5c2087a..0000000000
--- a/proofs/proof_global.mli
+++ /dev/null
@@ -1,121 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \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)         *)
-(************************************************************************)
-
-(** This module defines proof facilities relevant to the
-     toplevel. In particular it defines the global proof
-     environment. *)
-
-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 -> Constr.named_context 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], where
-    [id] is the name of the proof, [entries] the list of the proof terms
-    (in a form suitable for definitions). Together with the [terminator]
-    function which takes a [proof_object] together with a [proof_end]
-    (i.e. an proof ending command) and registers the appropriate
-    values. *)
-type 'a proof_entry = {
-  proof_entry_body   : 'a Entries.const_entry_body;
-  (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
-  (* State id on which the completion of type checking is reported *)
-  proof_entry_feedback : Stateid.t option;
-  proof_entry_type        : Constr.types option;
-  proof_entry_universes   : Entries.universes_entry;
-  proof_entry_opaque      : bool;
-  proof_entry_inline_code : bool;
-}
-
-(** When a proof is closed, it is reified into a [proof_object] *)
-type proof_object =
-  { name : Names.Id.t
-  (** name of the proof *)
-  ; entries : Evd.side_effects proof_entry list
-  (** list of the proof terms (in a form suitable for definitions). *)
-  ; poly : bool
-  (** polymorphic status *)
-  ; universes: UState.t
-  (** universe state *)
-  ; udecl : UState.universe_decl
-  (** universe declaration *)
-  }
-
-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 -> Future.fix_exn -> 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 = (Constr.t * Evd.side_effects) list * UState.t
-
-(* If allow_partial is set (default no) then an incomplete proof
- * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> t -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> 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) + a list of
- * ids to be cleared *)
-val set_used_variables : t ->
-  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 0ce726db25..756fef0511 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -6,9 +6,7 @@ Proof
 Logic
 Goal_select
 Proof_bullet
-Proof_global
 Refiner
 Tacmach
-Pfedit
 Clenv
 Clenvtac