aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index f168aff80..c082893ba 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -87,8 +87,11 @@ val interrupter : (int -> unit) ref
(** * Calls to Coqtop, cf [Serialize] for more details *)
+type logger = Interface.message_level -> string -> unit
+(** Except for interp, we use the default logger for any call. *)
+
val interp :
- handle -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
+ handle -> logger -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
val rewind : handle -> int -> int Interface.value
val status : handle -> Interface.status Interface.value
val goals : handle -> Interface.goals option Interface.value