diff options
Diffstat (limited to 'parsing/g_prim.mlg')
| -rw-r--r-- | parsing/g_prim.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index cc59b2175b..044758f11a 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -127,11 +127,11 @@ GRAMMAR EXTEND Gram [ [ i = bignat -> { my_int_of_string ~loc i } ] ] ; bigint: - [ [ i = NUMERAL -> { my_to_nat_string true ~loc i } - | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ] + [ [ i = NUMBER -> { my_to_nat_string true ~loc i } + | test_minus_nat; "-"; i = NUMBER -> { "-" ^ my_to_nat_string ~loc false i } ] ] ; bignat: - [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ] + [ [ i = NUMBER -> { my_to_nat_string ~loc true i } ] ] ; bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] |