Update fullGrammar, common.edit_mlg and orderedGrammar...

following changes to attribute parsing.

3 files changed, 25 insertions, 46 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 853b818498..5bf122078d 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -387,7 +387,7 @@ gallina: [
 | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ]
 | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ]
 | DELETE assumptions_token inline assum_list
-| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with"
+| REPLACE finite_token LIST1 inductive_definition SEP "with"
 | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
 |   "Variant" inductive_definition LIST0 ( "with" inductive_definition )
@@ -405,11 +405,6 @@ gallina: [
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
 ]
 
-DELETE: [
-| private_token
-| cumulativity_token
-]
-
 constructor_list_or_record_decl: [
 | OPTINREF
 ]
@@ -737,12 +732,8 @@ assumption_token: [
 | WITH [ "Variable" | "Variables" ]
 ]
 
-legacy_attrs: [
-| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private"
-]
-
 all_attrs: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr
 ]
 
 vernacular: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 32468690fb..2fabf92b7f 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -730,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 "."
@@ -769,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"
@@ -898,16 +899,6 @@ finite_token: [
 | "Class"
 ]
 
-cumulativity_token: [
-| "Cumulative"
-| "NonCumulative"
-]
-
-private_token: [
-| "Private"
-|
-]
-
 def_body: [
 | binders ":=" reduce lconstr
 | binders ":" lconstr ":=" reduce lconstr
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 "."