diff options
| author | coqbot-app[bot] | 2020-10-04 20:01:35 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-04 20:01:35 +0000 |
| commit | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (patch) | |
| tree | 44d20f3ea71f1c65b85c564c5f3d376dc8e57191 /doc/sphinx/user-extensions | |
| parent | e596bbb66b8a0ea6fe396315972f7743f8258a97 (diff) | |
| parent | 5b194f6c4f16b99fe8ebe3c8004c31c01aec0b3b (diff) | |
Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6ba53b581b..5148fa84c9 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -429,10 +429,6 @@ Displaying information about notations productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` and `tactic_then_gen` which are not shown and can't be printed. - The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify - what part of the grammar a nonterminal is from. If you examine nonterminal definitions - in the source code, they are identified only by the name following the colon. - Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the source code, edits it and inserts it into the documentation files. While the @@ -467,11 +463,11 @@ Displaying information about notations `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic:tactic_expr is + Entry tactic_expr is [ "5" RIGHTA - [ tactic:binder_tactic ] + [ binder_tactic ] | "4" LEFTA - [ SELF; ";"; tactic:binder_tactic + [ SELF; ";"; binder_tactic | SELF; ";"; SELF | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA |