diff options
| author | Théo Zimmermann | 2020-04-21 18:56:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-21 18:56:50 +0200 |
| commit | ab81744bb89e64651ad6a94cfd6771a668b8c74f (patch) | |
| tree | 212a27436bb0ce705555cf4290dfc4c3ff284472 | |
| parent | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (diff) | |
Update common.edit_mlg and fullGrammar following #12038.
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 18 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 12 |
2 files changed, 15 insertions, 15 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5034d9a3c9..700170b3c6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -906,14 +906,14 @@ command: [ | DELETE "Unset" option_table | REPLACE "Set" option_table option_setting | WITH OPT "Export" "Set" option_table (* set flag *) -| REPLACE "Test" option_table "for" LIST1 option_ref_value -| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value ) +| REPLACE "Test" option_table "for" LIST1 table_value +| WITH "Test" option_table OPT ( "for" LIST1 table_value ) | DELETE "Test" option_table (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Add" IDENT IDENT LIST1 option_ref_value -| WITH "Add" option_table LIST1 option_ref_value -| DELETE "Add" IDENT LIST1 option_ref_value +| REPLACE "Add" IDENT IDENT LIST1 table_value +| WITH "Add" option_table LIST1 table_value +| DELETE "Add" IDENT LIST1 table_value | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident @@ -969,9 +969,9 @@ command: [ | DELETE "Preterm" (* hide the fact that table names are limited to 2 IDENTs *) -| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value -| WITH "Remove" option_table LIST1 option_ref_value -| DELETE "Remove" IDENT LIST1 option_ref_value +| REPLACE "Remove" IDENT IDENT LIST1 table_value +| WITH "Remove" option_table LIST1 table_value +| DELETE "Remove" IDENT LIST1 table_value | DELETE "Restore" "State" IDENT | DELETE "Restore" "State" ne_string | "Restore" "State" [ IDENT | ne_string ] @@ -1550,7 +1550,7 @@ SPLICE: [ | constructor_type | record_binder | at_level_opt -| option_ref_value +| table_value | positive_search_mark | in_or_out_modules | option_setting diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 04c20a7203..4274dccb40 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -524,12 +524,12 @@ command: [ | "Set" option_table option_setting | "Unset" option_table | "Print" "Table" option_table -| "Add" IDENT IDENT LIST1 option_ref_value -| "Add" IDENT LIST1 option_ref_value -| "Test" option_table "for" LIST1 option_ref_value +| "Add" IDENT IDENT LIST1 table_value +| "Add" IDENT LIST1 table_value +| "Test" option_table "for" LIST1 table_value | "Test" option_table -| "Remove" IDENT IDENT LIST1 option_ref_value -| "Remove" IDENT LIST1 option_ref_value +| "Remove" IDENT IDENT LIST1 table_value +| "Remove" IDENT LIST1 table_value | "Write" "State" IDENT | "Write" "State" ne_string | "Restore" "State" IDENT @@ -1318,7 +1318,7 @@ option_setting: [ | STRING ] -option_ref_value: [ +table_value: [ | global | STRING ] |