diff options
Diffstat (limited to 'toplevel/coqloop.mli')
| -rw-r--r-- | toplevel/coqloop.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index e40353e0f..eb61084e0 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -15,7 +15,7 @@ open Pp type input_buffer = { mutable prompt : unit -> string; - mutable str : string; (** buffer of already read characters *) + mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) @@ -32,6 +32,8 @@ val set_prompt : (unit -> string) -> unit val print_toplevel_error : Exninfo.iexn -> std_ppcmds +val coqloop_feed : Feedback.feedback -> unit + (** Parse and execute one vernac command. *) val do_vernac : unit -> unit |