6 files changed, 20 insertions, 53 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 6e76d04e77..da798a238e 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}
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 04a8a25c12..5b73ac00a6 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt
   Collapse the universe hierarchy of {\Coq}. Warning: this makes the
   logic inconsistent.
 
+\item[{\tt -mangle-names} {\em ident}]\ %
+
+  Experimental: Do not depend on this option.
+
+  Replace Coq's auto-generated name scheme with names of the form
+  {\tt ident0}, {\tt ident1}, \ldots etc.
+  The command {\tt Set Mangle Names}\optindex{Mangle Names} turns
+  the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"}
+  \optindex{Mangle Names Prefix} changes the used prefix.
+
+  This feature is intended to be used as a linter for developments that want
+  to be robust to changes in the auto-generated name scheme. The options are
+  provided to facilitate tracking down problems.
+
 \item[{\tt -compat} {\em version}]\ %
 
   Attempt to maintain some backward-compatibility with a previous version.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c4c0435c5f..0a4d0ef9aa 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas.
 It may be useful to generate lemmas minimal w.r.t. the assumptions they depend
 on. This can be obtained thanks to the option below.
 
-\begin{quote}
-\optindex{Shrink Abstract}
-{\tt Set Shrink Abstract}
-\end{quote}
-\emph{Deprecated since 8.7}
-
-When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
-and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
-variables that appear in the term constructed by \texttt{\tacexpr}.
-
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 6b24fdde79..bd74a40d7c 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -298,15 +298,19 @@ subgoals which clutter your screen.
 \begin{Variant}
 \item {\tt Focus {\num}.}\\ 
 This focuses the attention on the $\num^{th}$ subgoal to prove.
-
 \end{Variant}
 
+\emph{This command is deprecated since 8.8: prefer the use of bullets or
+  focusing brackets instead, including {\tt {\num}: \{}}.
+
 \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
 This command restores to focus the goal that were suspended by the
 last {\tt Focus} command.
 
+\emph{This command is deprecated since 8.8.}
+
 \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
-Succeeds in the proof is fully unfocused, fails is there are some
+Succeeds in the proof if fully unfocused, fails if there are some
 goals out of focus.
 
 \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 30724759d2..6004711235 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
 \optindex{Boolean Equality Schemes}
 \optindex{Elimination Schemes}
 \optindex{Nonrecursive Elimination Schemes}
-\optindex{Record Elimination Schemes}
 \optindex{Case Analysis Schemes}
 \optindex{Decidable Equality Schemes}
 \optindex{Rewriting Schemes}
@@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
 declaration of the induction principles. It can be activated with the
 command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
-{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}.
 
 In addition, the {\tt Case Analysis Schemes} flag governs the generation of
 case analysis lemmas for inductive types, i.e. corresponding to the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6dca314b4a..40ba43b6cd 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4589,7 +4589,6 @@ incompatibilities.
 \end{Variants}
 
 \optindex{Intuition Negation Unfolding}
-\optindex{Intuition Iff Unfolding}
 
 Some aspects of the tactic {\tt intuition} can be
 controlled using options. To avoid that inner negations which do not
@@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones
 To avoid that inner occurrence of {\tt iff} which do not need to be
 unfolded are unfolded (this is the default), use:
 
-\begin{quote}
-{\tt Unset Intuition Iff Unfolding}
-\end{quote}
-
-To do that all negations of the goal are unfolded even inner ones
-(this is the default), use:
-
-\begin{quote}
-{\tt Set Intuition Iff Unfolding}
-\end{quote}
-
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}