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/fullGrammar | |
| 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/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 48 |
1 files changed, 17 insertions, 31 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 6897437457..2fabf92b7f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -386,11 +386,6 @@ fullyqualid: [ | ident ] -basequalid: [ -| ident fields -| ident -] - name: [ | "_" | ident @@ -401,6 +396,10 @@ reference: [ | ident ] +qualid: [ +| reference +] + by_notation: [ | ne_string OPT [ "%" IDENT ] ] @@ -410,10 +409,6 @@ smart_global: [ | by_notation ] -qualid: [ -| basequalid -] - ne_string: [ | STRING ] @@ -436,7 +431,7 @@ lstring: [ integer: [ | NUMERAL -| "-" NUMERAL +| test_minus_nat "-" NUMERAL ] natural: [ @@ -735,21 +730,22 @@ attribute_value: [ | ] -vernac: [ -| "Local" vernac_poly -| "Global" vernac_poly -| vernac_poly +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] -vernac_poly: [ -| "Polymorphic" vernac_aux -| "Monomorphic" vernac_aux -| vernac_aux +vernac: [ +| LIST0 legacy_attr vernac_aux ] vernac_aux: [ -| "Program" gallina "." -| "Program" gallina_ext "." | gallina "." | gallina_ext "." | command "." @@ -774,7 +770,7 @@ gallina: [ | assumptions_token inline assum_list | def_token ident_decl def_body | "Let" identref def_body -| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| finite_token LIST1 inductive_definition SEP "with" | "Fixpoint" LIST1 rec_definition SEP "with" | "Let" "Fixpoint" LIST1 rec_definition SEP "with" | "CoFixpoint" LIST1 corec_definition SEP "with" @@ -903,16 +899,6 @@ finite_token: [ | "Class" ] -cumulativity_token: [ -| "Cumulative" -| "NonCumulative" -] - -private_token: [ -| "Private" -| -] - def_body: [ | binders ":=" reduce lconstr | binders ":" lconstr ":=" reduce lconstr |