6 files changed, 7 insertions, 54 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-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>