diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 16:35:38 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-13 16:35:38 -0400 |
| commit | 0d32ecd637b05214228912e80a3d56fda60735e9 (patch) | |
| tree | 1e5fbeba442a0a18c30e916d902b5094a395d9c1 /parsing | |
| parent | 2ea5dc1e8f1f768725abef013db9dbdbdc55add2 (diff) | |
| parent | 154aeaad0802e621d09048e1e32485946a3ec443 (diff) | |
Merge PR #11688: When parsing a negative integer, ensure that the minus sign is contiguous to the number.
Reviewed-by: ejgallego
Diffstat (limited to 'parsing')
| -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) } ] ] |