diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-23 15:34:26 +0100 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-04 19:40:22 +0100 |
commit | 84e9fc5da618e9e2248ba4a650b07b6b5528f957 (patch) | |
tree | fef97f79ef48048c98e6ca2c5238d544e3294dc7 /doc | |
parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) |
Remove deprecated options related to typeclasses.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/Classes.tex | 27 |
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} |