8 files changed, 21 insertions, 64 deletions
diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e6690..0aa0d629e8 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
-Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
-documents (the LaTeX source and the PostScript, PDF and html outputs)
-are copyright (c) INRIA 2004-2006. The material connected to the FAQ
-(Coq for the Clueless) may be distributed only subject to the terms
-and conditions set forth in the Open Publication License, v1.0 or
-later (the latest version is presently available at
-http://www.opencontent.org/openpub/). Options A and B are *not*
-elected.
-
 The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
 Castéran and Eduardo Gimenez. All related documents (the LaTeX and
 BibTeX sources and the PostScript, PDF and html outputs) are copyright
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-oth.tex b/doc/refman/RefMan-oth.tex
index 1cd23c9297..bef31d3fa5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching
 successively in each of the directories specified in the {\em
   loadpath}. (see Section~\ref{loadpath})
 
+Files loaded this way cannot leave proofs open, and neither the {\tt
+  Load} command can be use inside a proof.
+
 \begin{Variants}
 \item {\tt Load {\str}.}\label{Load-str}\\
   Loads the file denoted by the string {\str}, where {\str} is any
@@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em
 
 \begin{ErrMsgs}
 \item \errindex{Can't find file {\ident} on loadpath}
+\item \errindex{Load is not supported inside proofs}
+\item \errindex{Files processed by Load cannot leave open proofs}
 \end{ErrMsgs}
 
 \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
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 66a5f107a5..40ba43b6cd 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal.
       rewrite H in H2 at - 2}. In particular a failure will happen if any of
     these three simpler tactics fails.
   \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
-      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+      H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen
     as soon as at least one of these simpler tactics succeeds.
   \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
     and \texttt{rewrite H in * |-} that succeeds if at
@@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
 \item applying the abstracted goal to {\term}
 \end{enumerate}
 
-For instance, if the current goal $T$ is expressible has $\phi(t)$
+For instance, if the current goal $T$ is expressible as $\phi(t)$
 where the notation captures all the instances of $t$ in $\phi(t)$,
 then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
 x}$)$) $t$}.  This command can be used, for instance, when the tactic
@@ -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}
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 95e541f81d..a2739e457e 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -596,7 +596,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq85.v
     theories/Compat/Coq86.v
     theories/Compat/Coq87.v
   </dd>