From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:43:01 +0200
Subject: [declare] Reify Proof.t API into the Proof module.

This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
---
 ide/coqide/idetop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

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)
   )
-- 
cgit v1.2.3