From a34ba68fd83f6044da3255c4a0f91c141aafceda Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Mar 2020 11:11:19 +0100
Subject: Documenting new primitive entry evaluable_ref usable for tactic
 notations.

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

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`
-- 
cgit v1.2.3