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/fullGrammar | |
| parent | 3b766fd8859b692e3e93cf83bf87d393e32c572e (diff) | |
[string notation] Handle parameterized inductives and non inductives
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3a0c3a8bc7..826a0b6f36 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -688,7 +688,7 @@ command: [ | "Print" "Fields" (* ring plugin *) | "Number" "Notation" reference reference reference OPT number_options ":" ident | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier -| "String" "Notation" reference reference reference ":" ident +| "String" "Notation" reference reference reference OPT string_option ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) @@ -2555,25 +2555,29 @@ deprecated_number_modifier: [ | "(" "abstract" "after" bignat ")" ] -number_mapping: [ +number_string_mapping: [ | reference "=>" reference | "[" reference "]" "=>" reference ] -number_via: [ -| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +number_string_via: [ +| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]" ] number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] number_options: [ | "(" LIST1 number_modifier SEP "," ")" ] +string_option: [ +| "(" number_string_via ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) |