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 | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Add missing ";" in record grammar
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 6 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 2 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 6 |
3 files changed, 7 insertions, 7 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 *) ] 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: [ |