From 0801250ff9aec71a2ccc2e0227d8706e1fbac6be Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 9 Jul 2018 14:08:58 -0400 Subject: Fix rst syntax for `quote ident {ident}` --- doc/sphinx/proof-engine/tactics.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- cgit v1.2.3