diff options
| author | Pierre-Marie Pédrot | 2020-03-20 15:52:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-20 15:52:42 +0100 |
| commit | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (patch) | |
| tree | 9374846f74bc76efe4c4f3e8f5ffd7840014af5c /doc/tools/docgram/orderedGrammar | |
| parent | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (diff) | |
| parent | 4b37834a2ed6a275daec1c98fac19795f96712ce (diff) | |
Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f26a174722..c3634466cc 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -172,7 +172,7 @@ vernacular: [ ] all_attrs: [ -| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) LIST0 legacy_attr ] attr: [ @@ -184,8 +184,15 @@ attr_value: [ | "(" LIST0 attr SEP "," ")" ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] sort: [ @@ -338,20 +345,10 @@ pattern0: [ ] vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly -] - -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." |