diff options
Diffstat (limited to 'toplevel/ide_intf.mli')
| -rw-r--r-- | toplevel/ide_intf.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index b948464056..5039395a8a 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -17,8 +17,8 @@ type goals = type 'a call val raw_interp : string -> unit call -val interp : bool * string -> int call -val rewind : int -> int call +val interp : bool * string -> unit call +val rewind : int -> unit call val is_in_loadpath : string -> bool call val make_cases : string -> string list list call (** The status, for instance "Ready in SomeSection, proving Foo" *) @@ -38,8 +38,8 @@ type 'a value = type handler = { is_in_loadpath : string -> bool; raw_interp : string -> unit; - interp : bool * string -> int; - rewind : int -> int; + interp : bool * string -> unit; + rewind : int -> unit; read_stdout : unit -> string; current_goals : unit -> goals; current_status : unit -> string; |