aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/lexer.ml4
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-18 00:32:02 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-18 01:24:58 +0100
commit1730369cd4f7b62a076c93b2a0ece190ee08f7eb (patch)
tree31319000fda0d9c98753c490bda9cdf8f3ea80d1 /parsing/lexer.ml4
parentb5f6eb57a480d705be9362067e2fb887533c822c (diff)
Making the EXTEND macros almost self-contained.
Diffstat (limited to 'parsing/lexer.ml4')
-rw-r--r--parsing/lexer.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 232e9aee3..8b8b38c34 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -724,7 +724,7 @@ let strip s =
let terminal s =
let s = strip s in
- let () = match s with "" -> Errors.error "empty token." | _ -> () in
+ let () = match s with "" -> failwith "empty token." | _ -> () in
if is_ident_not_keyword s then IDENT s
else if is_number s then INT s
else KEYWORD s