aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/toplevel.mli')
-rw-r--r--toplevel/toplevel.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 63a87201b..3f2fa83ad 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -18,7 +18,7 @@ open Pcoq
(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)
-type input_buffer = {
+type input_buffer = {
mutable prompt : unit -> string;
mutable str : string; (* buffer of already read characters *)
mutable len : int; (* number of chars in the buffer *)