summaryrefslogtreecommitdiff
path: root/toplevel/ide_intf.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-12-29 10:57:43 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-12-29 10:57:43 +0100
commitbf12eb93f3f6a6a824a10878878fadd59745aae0 (patch)
tree279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /toplevel/ide_intf.mli
parente0d682ec25282a348d35c5b169abafec48555690 (diff)
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'toplevel/ide_intf.mli')
-rw-r--r--toplevel/ide_intf.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 26c6b671..7d0685b1 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -77,7 +77,7 @@ type handler = {
evars : unit -> evar list option;
hints : unit -> (hint list * hint) option;
status : unit -> status;
- search : search_flags -> search_answer list;
+ search : search_flags -> string coq_object list;
get_options : unit -> (option_name * option_state) list;
set_options : (option_name * option_value) list -> unit;
inloadpath : string -> bool;
@@ -104,7 +104,7 @@ val of_call : 'a call -> xml
val to_call : xml -> 'a call
val of_answer : 'a call -> 'a value -> xml
-val to_answer : xml -> 'a value
+val to_answer : xml -> 'a call -> 'a value
(** * Debug printing *)