diff options
| author | Théo Zimmermann | 2020-03-18 18:36:10 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-19 17:47:20 +0100 |
| commit | a5c131bef041b0985e96a5ab0e64e7e1fdc76b7a (patch) | |
| tree | ab8b9e278ed149d73c641ff316423fd225690e86 | |
| parent | 0fe5cfd5fa81565b6045bd602b786ed38e19aaa9 (diff) | |
Update fullGrammar and common.edit_mlg following #11839.
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 9 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 15 |
2 files changed, 9 insertions, 15 deletions
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: [ |