diff options
Diffstat (limited to 'doc/sphinx/language/core/records.rst')
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 4 |
1 files changed, 2 insertions, 2 deletions
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 |