aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-23 03:12:05 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-14 22:19:26 +0100
commit40fe374710c7d701e539dd92c085dfb6b244ffae (patch)
tree64e9fb4b621a6e3a9146dc608138d0abc856c646 /toplevel/coqloop.mli
parentf4c3d91fe94b9ec221f87365aac06d1884b9aaf8 (diff)
[safe_string] toplevel/coqloop
No functional change, even if we could optimize `blanch_utf8_string` a bit more by using `String.init`.
Diffstat (limited to 'toplevel/coqloop.mli')
-rw-r--r--toplevel/coqloop.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index e40353e0f..d248f2f70 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 *)