Minor doc improvement.

1 files changed, 10 insertions, 8 deletions

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 3e9b859d27..a5e9023732 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -440,15 +440,19 @@ Typeclasses Transparent, Typeclasses Opaque
 
    This command makes the identifiers transparent during typeclass
    resolution.
+   Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`.
 
 .. cmd:: Typeclasses Opaque {+ @ident}
 
-   Make the identifiers opaque for typeclass search. It is useful when some
-   constants prevent some unifications and make resolution fail. It is also
-   useful to declare constants which should never be unfolded during
-   proof-search, like fixpoints or anything which does not look like an
-   abbreviation. This can additionally speed up proof search as the typeclass
-   map can be indexed by such rigid constants (see
+   Make the identifiers opaque for typeclass search.
+   Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`.
+
+   It is useful when some constants prevent some unifications and make
+   resolution fail. It is also useful to declare constants which
+   should never be unfolded during proof-search, like fixpoints or
+   anything which does not look like an abbreviation. This can
+   additionally speed up proof search as the typeclass map can be
+   indexed by such rigid constants (see
    :ref:`thehintsdatabasesforautoandeauto`).
 
 By default, all constants and local variables are considered transparent. One
@@ -458,8 +462,6 @@ type, like:
 .. coqdoc::
    Definition relation A := A -> A -> Prop.
 
-This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
-
 
 Settings
 ~~~~~~~~