aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli12
1 files changed, 6 insertions, 6 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 330cc776f..4fe6a2188 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -122,13 +122,13 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
type 'a query = 'a Interface.value task
(** A type abbreviation for coqtop specific answers *)
-val interp : ?logger:Ideutils.logger ->
- ?raw:bool ->
- ?verbose:bool ->
- Interface.edit_id -> string -> Interface.interp_rty query
-val backto : Interface.backto_sty -> Interface.backto_rty query
+val add : ?logger:Ideutils.logger ->
+ Interface.add_sty -> Interface.add_rty query
+val edit_at : Interface.edit_at_sty -> Interface.edit_at_rty query
+val query : ?logger:Ideutils.logger ->
+ Interface.query_sty -> Interface.query_rty query
val status : ?logger:Ideutils.logger ->
- Interface.status_sty -> Interface.status_rty query
+ Interface.status_sty -> Interface.status_rty query
val goals : ?logger:Ideutils.logger ->
Interface.goals_sty -> Interface.goals_rty query
val evars : Interface.evars_sty -> Interface.evars_rty query