4 files changed, 20 insertions, 22 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/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}