diff options
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 105bd4668e..8d4e0189e6 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -139,6 +139,14 @@ integer: [ ] natural: [ +| bignat +] + +bigint: [ +| OPT "-" bignat +] + +bignat: [ | [ decnat | hexnat ] ] @@ -1291,8 +1299,8 @@ field_mod: [ ] numeral_modifier: [ -| "(" "warning" "after" number ")" -| "(" "abstract" "after" number ")" +| "(" "warning" "after" bignat ")" +| "(" "abstract" "after" bignat ")" ] hints_path: [ |