diff options
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 88590fa4af..13f8359516 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -501,7 +501,7 @@ let rec next_token = parser bp (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) let () = match t with - | KEYWORD "." -> + | KEYWORD ("." | "...") -> if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; between_com := true; | _ -> () diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 07a398903c..de2a81b7c9 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -270,7 +270,7 @@ let print_toplevel_error e = (* Read the input stream until a dot is encountered *) let parse_to_dot = let rec dot st = match Compat.get_tok (Stream.next st) with - | Tok.KEYWORD "." -> () + | Tok.KEYWORD ("."|"...") -> () | Tok.EOI -> raise End_of_input | _ -> dot st in |