aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide/idetop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index bd99cbed1b..2adc35ae3e 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -343,7 +343,7 @@ let search flags =
let pstate = Vernacstate.Declare.get_pstate () in
let sigma, env = match pstate with
| None -> let env = Global.env () in Evd.(from_env env, env)
- | Some p -> Declare.get_goal_context p 1 in
+ | Some p -> Declare.Proof.get_goal_context p 1 in
List.map export_coq_object (Search.interface_search env sigma (
List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
)