aboutsummaryrefslogtreecommitdiff
path: root/vernac/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/search.ml')
-rw-r--r--vernac/search.ml2
1 files changed, 1 insertions, 1 deletions
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) =