Add missing ";" in record grammar

5 files changed, 10 insertions, 10 deletions

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
 
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a9f9c805d8..1e9be8dded 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -396,8 +396,8 @@ operconstr0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
-| WITH "{|" LIST0 field_def bar_cbrace
-| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
 | MOVETO term_generalizing "`{" operconstr200 "}"
 | MOVETO term_generalizing "`(" operconstr200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
@@ -585,7 +585,7 @@ constructor_list_or_record_decl: [
 
 record_fields: [
 | REPLACE record_field ";" record_fields
-| WITH LIST0 record_field SEP ";"
+| WITH LIST0 record_field SEP ";" OPT ";"
 | DELETE record_field
 | DELETE (* empty *)
 ]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 067050b4f5..73641976e3 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1740,11 +1740,11 @@ simple_tactic: [
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "rtauto"
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)
 | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
 | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
+| "rtauto"
 ]
 
 mlname: [
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: [