diff options
| author |  Joachim Breitner <mail@joachim-breitner.de> | 2018-07-09 14:08:58 -0400 |
|---|---|---|
| committer | Joachim Breitner <mail@joachim-breitner.de> | 2018-07-09 14:08:58 -0400 |
| commit | 0801250ff9aec71a2ccc2e0227d8706e1fbac6be (patch) | |
| tree | 1dd28f57a33cb01ea9b9f16c49512a3545bcd174 | |
| parent | c1d4dc68ace54f9ff9fd8f6466add38098ef0495 (diff) | |
Fix rst syntax for `quote ident {ident}`
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
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. |