From d7094a827db14523efe05a1a71cd18f4eb6637ea Mon Sep 17 00:00:00 2001
From: Zeimer
Date: Fri, 31 Aug 2018 09:39:17 +0200
Subject: Fixed the seealso directive in a few places.

---
 doc/sphinx/addendum/type-classes.rst            | 2 +-
 doc/sphinx/proof-engine/tactics.rst             | 4 ++--
 doc/sphinx/proof-engine/vernacular-commands.rst | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index d26105b651..ab4b4a9824 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -431,7 +431,7 @@ Typeclasses Transparent, Typclasses Opaque
 
 .. cmd:: Typeclasses Transparent {+ @ident}
 
-   This command defines makes the identifiers transparent during typeclass
+   This command makes the identifiers transparent during typeclass
    resolution.
 
 .. cmd:: Typeclasses Opaque {+ @ident}
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:
-- 
cgit v1.2.3