diff options
| author | Jim Fehrle | 2020-10-11 19:15:51 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:17:21 -0700 |
| commit | ede77b72328c98995c0636656bb71ba87861ddfe (patch) | |
| tree | 69510ffd33c71a461b22dea76d42656bf4d3293d /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | b402adc12c00ba72046423d3a1737ccad517f70e (diff) | |
Rename tactic_expr -> ltac_expr
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 94a705a4c6..fc5aa3f93d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -477,10 +477,10 @@ Displaying information about notations such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. For example, this output from `Print Grammar tactic` shows the first 3 levels for - `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + `ltac_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_expr is + Entry ltac_expr is [ "5" RIGHTA [ binder_tactic ] | "4" LEFTA |