diff options
| author | Zeimer | 2018-08-31 09:39:17 +0200 |
|---|---|---|
| committer | Zeimer | 2018-08-31 09:45:17 +0200 |
| commit | d7094a827db14523efe05a1a71cd18f4eb6637ea (patch) | |
| tree | a3185dcbc44a3956b7fc182e14eb3433fd12ddea | |
| parent | a67fa614450467afbd56233f489b2105dc655a58 (diff) | |
Fixed the seealso directive in a few places.
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 | ||||
| -rw-r--r-- | 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: |