diff options
| author | Hugo Herbelin | 2020-01-31 00:54:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-03 17:35:52 +0100 |
| commit | 154aeaad0802e621d09048e1e32485946a3ec443 (patch) | |
| tree | 798f4f551f6b2cc151a8a2ecca8710cf8eff0d86 | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
When parsing negative integer, ensure minus sign is contiguous to the number.
For instance, formerly, "Set Inline Level - 1" was succeeding. Now
only "Set Inline Level -1" succeeds. (Even though -1 does not make
sense for a Inline Level, but that's then a semantic issue. Other
options may accept negative numbers in general.)
| -rw-r--r-- | parsing/g_prim.mlg | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 5f61b9a047..7e0360af72 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -37,6 +37,12 @@ let test_pipe_closedcurly = lk_kw "|" >> lk_kw "}" >> check_no_space end +let test_minus_nat = + let open Pcoq.Lookahead in + to_entry "test_minus_nat" begin + lk_kw "-" >> lk_nat >> check_no_space + end + } GRAMMAR EXTEND Gram @@ -122,7 +128,7 @@ GRAMMAR EXTEND Gram ; integer: [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } - | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ] + | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ] ; natural: [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ] |