aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/plugin_tutorial/tuto1/src/g_tuto1.mlg2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--tactics/abstract.ml2
-rw-r--r--tactics/pfedit.ml74
-rw-r--r--tactics/pfedit.mli53
-rw-r--r--tactics/proof_global.ml71
-rw-r--r--tactics/proof_global.mli51
-rw-r--r--tactics/tactics.mllib2
-rw-r--r--toplevel/coqloop.ml6
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/vernacentries.ml16
-rw-r--r--vernac/vernacstate.ml2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:21:51 +0000