diff options
| author | Théo Zimmermann | 2020-07-23 09:30:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-07-23 09:30:32 +0200 |
| commit | b8962b4d7d4c23c01b03713fcd9a0816edad3f40 (patch) | |
| tree | d0f941ef4290d74d846f68538019d32b919442a3 /doc | |
| parent | 1ea5dec77580e479885ffbea0278174fdec629fb (diff) | |
| parent | a34ba68fd83f6044da3255c4a0f91c141aafceda (diff) | |
Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qualid in tactic notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fcd5ecc070..18149a690a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1786,13 +1786,13 @@ Tactic notations allow customizing the syntax of tactics. * - ``reference`` - :token:`qualid` - - a global reference of term - - :tacn:`unfold` + - a qualified identifier + - name of an |Ltac|-defined tactic * - ``smart_global`` - :token:`reference` - a global reference of term - - :tacn:`with_strategy` + - :tacn:`unfold`, :tacn:`with_strategy` * - ``constr`` - :token:`term` |