diff options
| author | Pierre Roux | 2020-09-03 13:14:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:16 +0100 |
| commit | c217bbe80e18255ee3e67fa6266736529d80636d (patch) | |
| tree | 3730ea847ac2dc75b52d6a9217c099fc53105ca1 /doc/tools/docgram/common.edit_mlg | |
| parent | 14f301450a356915d131e9f9326b3fa7234241a8 (diff) | |
[numeral notation] Document the via ... using ... option
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4d615a130a..e43583de09 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier -| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| 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 ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -number_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 @@ -2464,6 +2460,8 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_mapping +| number_options ] (* end SPLICE *) RENAME: [ |