diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-10 11:12:55 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-10 11:12:55 +0200 |
| commit | f796ad268922e167e2156de0b5beef4eeb001700 (patch) | |
| tree | ff5e1f830413739200707cae5daff5bf82f10004 | |
| parent | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (diff) | |
| parent | 0801250ff9aec71a2ccc2e0227d8706e1fbac6be (diff) | |
Merge PR #8025: 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. |