[proof] Move proof_global functionality to Proof_global from Pfedit

This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.

15 files changed, 144 insertions, 149 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 73d94c2a51..8015d62eb4 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,7 +286,7 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Pfedit.get_current_context pstate in
+    let sigma, env = Proof_global.get_current_context pstate in
     let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3a90d24c97..40dbf8bea4 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -729,7 +729,7 @@ let extract_and_compile l =
 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 sigma, env = Proof_global.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
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e85d94cd72..8abd68d28d 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -91,7 +91,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   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
+    try Proof_global.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
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index c139594f13..20975cbc57 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -10,8 +10,6 @@
 
 open Pp
 open Util
-open Names
-open Environ
 open Evd
 
 let use_unification_heuristics =
@@ -20,48 +18,6 @@ let use_unification_heuristics =
     ~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
@@ -105,39 +61,9 @@ let solve ?with_end_tac gi info_lvl tac pr =
     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
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index c49e997757..8d06a260da 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -16,30 +16,6 @@ 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. *)
@@ -48,38 +24,9 @@ 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
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 98de0c848b..78691d8c74 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -282,3 +282,74 @@ let update_global_env =
       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 (Pfedit.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 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
+
+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 { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise NoSuchGoal
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Refiner.pf_env { Evd.it=goal ; sigma=sigma; })
+
+let get_goal_context pf i =
+  let p = get_proof pf in
+  get_goal_context_gen p i
+
+let get_current_goal_context pf =
+  let p = 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 = get_proof pf in
+  get_proof_context p
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 874708ded8..c41a9c656e 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -96,3 +96,54 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
  * (w.r.t. type dependencies and let-ins covered by it) *)
 val set_used_variables : t ->
   Names.Id.t list -> Constr.named_context * t
+
+(** [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 -> t -> t * 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:Names.Id.t
+  -> ?opaque:opacity_flag
+  -> uctx:UState.t
+  -> sign:Environ.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
+  -> Environ.env
+  -> uctx:UState.t
+  -> poly:bool
+  -> typ:EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Constr.types option * bool * UState.t
+
+(** {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 : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_context : t -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_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 : t -> Evd.evar_map * Environ.env
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 0c4e496650..f9f2a78c35 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,7 +1,7 @@
 DeclareScheme
+Pfedit
 Declare
 Proof_global
-Pfedit
 Dnet
 Dn
 Btermdn
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b8acdd3af1..ff33663926 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -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_global.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_global.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_global.NoSuchGoal
   | Option.IsNone ->
     CErrors.user_err (str "No goals to show.")
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f3ad324aa5..2b661888e4 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) = Proof_global.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) = Proof_global.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) = Proof_global.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/lemmas.ml b/vernac/lemmas.ml
index 7f7340bb34..b0f33b7558 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -81,7 +81,7 @@ module Internal = struct
 end
 
 let by tac pf =
-  let proof, res = Pfedit.by tac pf.proof in
+  let proof, res = Proof_global.by tac pf.proof in
   { pf with proof }, res
 
 (************************************************************************)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 435085793c..e59c93c2e2 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
+      Proof_global.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/search.ml b/vernac/search.ml
index 68a30b4231..1e89cbd551 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 -> Proof_global.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/vernacentries.ml b/vernac/vernacentries.ml
index 6de14997d4..cbb578c109 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 -> Proof_global.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 -> Proof_global.get_goal_context p glnum
 
 let cl_of_qualid = function
   | FunClass -> Coercionops.CL_FUN
@@ -95,12 +95,12 @@ let show_proof ~pstate =
   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 sigma, env = Proof_global.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_global.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
+        Proof_global.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
@@ -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 -> Proof_global.get_goal_context lemma n
+    | None -> Proof_global.get_current_context lemma
 
 let query_command_selector ?loc = function
   | None -> None
@@ -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 = Proof_global.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 *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index a4e9c8e1ab..2987b3bc43 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -178,7 +178,7 @@ module Proof_global = struct
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
 
-  let get_current_context () = cc Pfedit.get_current_context
+  let get_current_context () = cc Proof_global.get_current_context
 
   let get_all_proof_names () =
     try cc_stack LemmaStack.get_all_proof_names