diff options
| author | Maxime Dénès | 2019-08-08 19:41:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-08-08 19:41:14 +0200 |
| commit | 9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (patch) | |
| tree | ebe5ff5638efedfad980f0e81c6bb278e3547eb2 /parsing/cLexer.ml | |
| parent | 0d61500c7137f93942a63a356226276c26edfd99 (diff) | |
| parent | 97d739835e98dcca038970a50e169a4e1127bd80 (diff) | |
Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involving &
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: ggonthier
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: vbgl
Diffstat (limited to 'parsing/cLexer.ml')
| -rw-r--r-- | parsing/cLexer.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index a27d6450b7..de23f05a9e 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -785,12 +785,14 @@ let next_token ~diff_mode loc s = (* Location table system for creating tables associating a token count to its location in a char stream (the source) *) -let locerr () = invalid_arg "Lexer: location function" +let locerr i = + let m = "Lexer: location function called on token "^string_of_int i in + invalid_arg m let loct_create () = Hashtbl.create 207 let loct_func loct i = - try Hashtbl.find loct i with Not_found -> locerr () + try Hashtbl.find loct i with Not_found -> locerr i let loct_add loct i loc = Hashtbl.add loct i loc |