diff options
| author | Pierre Roux | 2020-09-03 13:27:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:51 +0100 |
| commit | b6214bd4d5d3003e9b60411a717e84277feead24 (patch) | |
| tree | cd0a04bbf1b9e43d21ec5944c4458d74797c5b09 /doc/tools/docgram/common.edit_mlg | |
| parent | 3b766fd8859b692e3e93cf83bf87d393e32c572e (diff) | |
[string notation] Handle parameterized inductives and non inductives
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index e43583de09..5de1f09c53 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1289,8 +1289,8 @@ command: [ | 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 +| 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 *) @@ -2460,8 +2460,9 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) -| number_mapping +| number_string_mapping | number_options +| string_option ] (* end SPLICE *) RENAME: [ |