diff options
| author | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
| commit | bdc5db891aa2a060387da758d8910a82cea21da1 (patch) | |
| tree | 8122c3a46ee68b7b5f0f3c263d8516a40e08347c /doc/tools/docgram/common.edit_mlg | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Add missing ";" in record grammar
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 6 |
1 files changed, 3 insertions, 3 deletions
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 *) ] |