diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-21 16:36:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 12:28:15 +0100 |
| commit | 0ac79cca3c9f135df4138d1e43afc2b912766974 (patch) | |
| tree | 99fd8d39594d0b293333aab9d8325ae0238ed39f /doc | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Fix typo in doc optindex for Typeclass Resolution ...
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Classes.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 22c75b4fc..d4d7fbd88 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -519,14 +519,14 @@ potentially more expensive proof-search (i.e. more useless backtracking). \subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclasses Resolution After Apply} +\optindex{Typeclass Resolution After Apply} \emph{Deprecated since 8.6} This option (off by default in Coq 8.6 and 8.5) controls the resolution of typeclass subgoals generated by the {\tt apply} tactic. \subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclasses Resolution For Conversion} +\optindex{Typeclass Resolution For Conversion} This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during |