From a5c131bef041b0985e96a5ab0e64e7e1fdc76b7a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 18:36:10 +0100
Subject: Update fullGrammar and common.edit_mlg following #11839.

---
 doc/tools/docgram/common.edit_mlg | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fe2e68a517..853b818498 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -140,10 +140,10 @@ field_ident: [
 | "." ident
 ]
 
-basequalid: [
-| REPLACE ident fields
-| WITH ident LIST0 field_ident
-| DELETE ident
+qualid: [ | DELETENT ]
+
+qualid: [
+| ident LIST0 field_ident
 ]
 
 field: [ | DELETENT ]
@@ -842,7 +842,6 @@ SPLICE: [
 | ne_lstring
 | ne_string
 | lstring
-| basequalid
 | fullyqualid
 | global
 | reference
-- 
cgit v1.2.3


From 82960d49d08372c345da972f16c3fbcc1c2073b1 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 18:36:10 +0100
Subject: Update fullGrammar, common.edit_mlg and orderedGrammar...

following changes to attribute parsing.
---
 doc/tools/docgram/common.edit_mlg | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

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: [
-- 
cgit v1.2.3