aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/proof-engine/tactics.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 45667b099..485a78c22 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4190,7 +4190,7 @@ datatype: see :ref:`quote` for the full details.
Happens when quote is not able to perform inversion properly.
-.. tacv:: quote ident {* @ident}
+.. tacv:: quote @ident {* @ident}
All terms that are built only with :n:`{* @ident}` will be considered by quote
as constants rather than variables.