diff options
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 18 |
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 ~~~~~~~~ |