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