Merge PR #6824: Remove deprecated options related to typeclasses.

1 files changed, 0 insertions, 27 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 6e76d04e7..da798a238 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -492,26 +492,6 @@ control on the triggering of instances.  For example, forcing a constant
 to explicitely appear in the pattern will make it never apply on a goal
 where there is a hole in that place.
 
-\subsection{\tt Set Typeclasses Legacy Resolution}
-\optindex{Typeclasses Legacy Resolution}
-\emph{Deprecated since 8.7}
-
-This option (off by default) uses the 8.5 implementation of resolution.
-Use for compatibility purposes only (porting and debugging).
-
-\subsection{\tt Set Typeclasses Module Eta}
-\optindex{Typeclasses Modulo Eta}
-\emph{Deprecated since 8.7}
-
-This option allows eta-conversion for functions and records during
-unification of type-classes. This option is unsupported since 8.6 with
-{\tt Typeclasses Filtered Unification} set, but still affects the
-default unification strategy, and the one used in {\tt Legacy
-  Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
-  Filtered Unification} is set, this has no effect and unification will
-find solutions up-to eta conversion. Note however that syntactic
-pattern-matching is not up-to eta.
-
 \subsection{\tt Set Typeclasses Limit Intros}
 \optindex{Typeclasses Limit Intros}
 
@@ -525,13 +505,6 @@ invertibility status of the product introduction rule, resulting in
 potentially more expensive proof-search (i.e. more useless
 backtracking).
 
-\subsection{\tt Set Typeclass 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{Typeclass Resolution For Conversion}