diff options
| author | coqbot-app[bot] | 2020-11-05 15:32:31 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-05 15:32:31 +0000 |
| commit | afc828b3e207dd39c59d1501d570a88b2012fd2c (patch) | |
| tree | f9af32a8b25439a9eb6c8407f99ad94f78a64fda /doc/tools/docgram/common.edit_mlg | |
| parent | b95c38d3d28a59da7ff7474ece0cb42623497b7d (diff) | |
| parent | e6f7517be65e9f5d2127a86e2213eb717d37e43f (diff) | |
Merge PR #12218: Numeral notations for non inductive types
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a143a6c7cf..97d479b238 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,12 +1285,12 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "String" "Notation" reference reference reference ":" ident -| WITH "String" "Notation" reference reference reference ":" scope_name +| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident +| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name +| REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier +| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident +| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) | DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -numeral_modifier: [ -| OPTINREF -] - binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 @@ -2465,6 +2461,9 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_string_mapping +| number_options +| string_option ] (* end SPLICE *) RENAME: [ |