diff options
| author | Maxime Dénès | 2017-12-15 17:47:27 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-15 17:47:27 +0100 |
| commit | 484d69c8e59823f0a1fb4f1b99b371c8bdecd880 (patch) | |
| tree | 46fc70a88ea96691c12e6424e5c05cc00c514574 /doc/refman/Classes.tex | |
| parent | 5ae35a94dd3ec72d9ac91ba3b34674dd79a78263 (diff) | |
| parent | 539a62a79f75f9f5190b9bd8edfbb04b880a5f1f (diff) | |
Merge PR #6219: Document undocumented options
Diffstat (limited to 'doc/refman/Classes.tex')
| -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 cab6739998..6e76d04e77 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -526,14 +526,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 |