aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/fullGrammar
diff options
context:
space:
mode:
authorJim Fehrle2020-02-26 11:15:22 -0800
committerJim Fehrle2020-03-25 09:41:19 -0700
commite49cd002cb1ce6e06fec0e735bc6353c59416a6a (patch)
tree8b2015d2669c142f3c72b832978ae45fdebee828 /doc/tools/docgram/fullGrammar
parentbc70bb31c579b9482d0189f20806632c62b26a61 (diff)
Convert Gallina Extensions to use prodn
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
-rw-r--r--doc/tools/docgram/fullGrammar14
1 files changed, 9 insertions, 5 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2fabf92b7f..241cf48cf1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -430,17 +430,21 @@ lstring: [
]
integer: [
-| NUMERAL
-| test_minus_nat "-" NUMERAL
+| bigint
]
natural: [
-| NUMERAL
+| bignat
| _natural
]
bigint: [
| NUMERAL
+| test_minus_nat "-" NUMERAL
+]
+
+bignat: [
+| NUMERAL
]
bar_cbrace: [
@@ -2516,7 +2520,7 @@ field_mods: [
numnotoption: [
|
-| "(" "warning" "after" bigint ")"
-| "(" "abstract" "after" bigint ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
]