diff options
| author | Hugo Herbelin | 2020-03-15 11:11:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-17 18:07:21 +0200 |
| commit | a34ba68fd83f6044da3255c4a0f91c141aafceda (patch) | |
| tree | cef39208a9f2a0d3d95c4821219a2b34518db808 /doc | |
| parent | e221ebd6c8b485274b809768c965f2653094fd8f (diff) | |
Documenting new primitive entry evaluable_ref usable for tactic notations.
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` |