diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 854c3c919c..241cdf5eea 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3291,7 +3291,7 @@ command. Performs all the rewriting in the clause :n:`@clause`. The clause argument must not contain any ``type of`` nor ``value of``. -.. seealso: +.. seealso:: :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. @@ -3729,7 +3729,7 @@ Setting implicit automation tactics In this case the tactic command typed by the user is equivalent to ``tactic``:sub:`1` ``;tactic``. - .. seealso:: ``Proof`` in :ref:`proof-editing-mode`. + .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. .. cmdv:: Proof with tactic using {+ @ident} diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 87131879e2..584193b9c6 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1131,7 +1131,7 @@ described first. There is no constant referred by :n:`@qualid` in the environment. - .. seealso: + .. seealso:: Sections :ref:`performingcomputations`, :ref:`tactics-automating`, :ref:`proof-editing-mode` @@ -1198,7 +1198,7 @@ described first. nothing prevents the user to also perform a ``Ltac`` `ident` ``:=`` `convtactic`. - .. seealso: :ref:`performingcomputations` + .. seealso:: :ref:`performingcomputations` .. _controlling-locality-of-commands: |