diff options
| author | Hugo Herbelin | 2020-01-31 01:04:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 2a31e23df8ff0ab67a09008858fa49e77e5f4332 (patch) | |
| tree | 30e6e02d0740a87f7d9325cce87266d329990baa /plugins | |
| parent | 7ba059507b67b1f6ea3566a5d1dee40f6af78316 (diff) | |
Adding bignat to parse positive numbers; bigint now includes negative ints.
Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 49d29e7b63..eccefdf64a 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -29,8 +29,8 @@ let pr_numnot_option = function VERNAC ARGUMENT EXTEND numnotoption PRINTED BY { pr_numnot_option } | [ ] -> { Nop } -| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } -| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning waft } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract n } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF |