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 /doc/tools/docgram/fullGrammar | |
| parent | 0fe5cfd5fa81565b6045bd602b786ed38e19aaa9 (diff) | |
Update fullGrammar and common.edit_mlg following #11839.
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 15 |
1 files changed, 5 insertions, 10 deletions
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: [ |