From bdc5db891aa2a060387da758d8910a82cea21da1 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 12 Oct 2020 10:37:09 -0700
Subject: Add missing ";" in record grammar

---
 doc/sphinx/language/core/inductive.rst | 2 +-
 doc/sphinx/language/core/records.rst   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 4cdfba146a..39b154de8d 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -13,7 +13,7 @@ Inductive types
    .. prodn::
       inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
-      | {? @ident } %{ {*; @record_field } %}
+      | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
 
    This command defines one or more
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index cd44d06e67..b2099b8636 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    .. insertprodn record_definition field_def
 
    .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
+      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations }
       record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
       | {* @binder } := @term
-      term_record ::= %{%| {* @field_def } %|%}
+      term_record ::= %{%| {*; @field_def } {? ; } %|%}
       field_def ::= @qualid {* @binder } := @term
 
 
-- 
cgit v1.2.3