diff options
| author | Vincent Laporte | 2019-04-29 12:34:51 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 12:34:51 +0000 |
| commit | 530d72a251038f31e5dfe9d3b982ca744df01e59 (patch) | |
| tree | 485c707b66f99063b8cc95c74f93c2f69a3aa148 | |
| parent | 686894d47cfa548b4fa510c06c6bb08194dee5f7 (diff) | |
| parent | 86cd7608cb2ccb53385fff73df7eb4adc662e343 (diff) | |
Merge PR #10011: [refman] Fix typo.
Reviewed-by: vbgl
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b069cf27f4..a5e9023732 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -433,22 +433,26 @@ few other commands related to typeclasses. .. _TypeclassesTransparent: -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Typeclasses Transparent, Typeclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses Transparent {+ @ident} 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 ~~~~~~~~ |