aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/orderedGrammar
diff options
context:
space:
mode:
authorJim Fehrle2020-10-12 10:37:09 -0700
committerJim Fehrle2020-10-12 10:37:09 -0700
commitbdc5db891aa2a060387da758d8910a82cea21da1 (patch)
tree8122c3a46ee68b7b5f0f3c263d8516a40e08347c /doc/tools/docgram/orderedGrammar
parent03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff)
Add missing ";" in record grammar
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
-rw-r--r--doc/tools/docgram/orderedGrammar6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index cbef29fb39..61befe9f1f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -539,7 +539,7 @@ variant_definition: [
]
record_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
+| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations
]
record_field: [
@@ -553,7 +553,7 @@ field_body: [
]
term_record: [
-| "{|" LIST0 field_def "|}"
+| "{|" LIST0 field_def SEP ";" OPT ";" "|}"
]
field_def: [
@@ -566,7 +566,7 @@ inductive_definition: [
constructors_or_record: [
| OPT "|" LIST1 constructor SEP "|"
-| OPT ident "{" LIST0 record_field SEP ";" "}"
+| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}"
]
constructor: [