Fixed the seealso directive in a few places.

1 files changed, 2 insertions, 2 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}