aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-04-23 23:38:26 +0200
committerPierre-Marie Pédrot2021-04-23 23:38:26 +0200
commitd9e9a63f9f49768eee8b239812365ad1115b964f (patch)
tree0d608882d4aa094ee6c519005696f272f14a2d27 /toplevel/coqloop.ml
parent528f8384dcd817e4e339719a5d99c30d48520a8e (diff)
parent4ca8b4aab1a6b4f55aab026e42a530fa125553c0 (diff)
Merge PR #14075: New level of abstraction for streams with (non-canonical) location function
Reviewed-by: ppedrot
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4faecd2e62..0265c0063c 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -242,12 +242,12 @@ let set_prompt prompt =
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
- let rec dot tok st = match Stream.next st with
+ let rec dot st = match LStream.next st with
| Tok.KEYWORD ("."|"...") -> ()
| Tok.EOI -> ()
- | _ -> dot tok st
+ | _ -> dot st
in
- Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
+ Pcoq.Entry.(of_parser "Coqtoplevel.dot" { parser_fun = dot })
(* If an error occurred while parsing, we try to read the input until a dot
token is encountered.