diff options
| author | Théo Zimmermann | 2020-06-09 12:42:36 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-09 12:42:36 +0200 |
| commit | 4642ce1c5924cbfa93d6a8e96cf86839e614623b (patch) | |
| tree | 4993e6de8cd61b655733feb5efce2e9c85f57cef /doc/tools/docgram/README.md | |
| parent | 10e126ba3232dac847ce5c7a62ff97d9ddfaa620 (diff) | |
| parent | 27d6686f399f40904ff6005a84677907d53c5bbf (diff) | |
Merge PR #12103: Convert Ltac chapter to prodn
Diffstat (limited to 'doc/tools/docgram/README.md')
| -rw-r--r-- | doc/tools/docgram/README.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 4cde3809f0..2d29743d78 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -200,6 +200,11 @@ that appear in the specified production: `MOVETO <destination> <production>` - moves the production to `<destination>` and, if needed, creates a new production <edited_nt> -> \<destination>. + +`MOVEALLBUT <destination>` - moves all the productions in the nonterminal to `<destination>` +*except* for the productions following the `MOVEALLBUT` production in the edit script +(terminated only by the closing `]`). + `OPTINREF` - verifies that <edited_nt> has an empty production. If so, it removes the empty production and replaces all references to <edited_nt> throughout the grammar with `OPT <edited_nt>` |