diff options
| -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) } ] ] |