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 ++++-----
 doc/tools/docgram/fullGrammar     | 15 +++++----------
 2 files changed, 9 insertions(+), 15 deletions(-)

(limited to 'doc')

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
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 6897437457..32468690fb 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: [
-- 
cgit v1.2.3