5 files changed, 23 insertions, 2 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 3a99bfdd4f..11dd3a0517 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified.
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
 \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
-  Control whether obligations defined by tactics should have their
+  Control whether obligations should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
 \end{itemize}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5880487f71..2f07beb725 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1041,6 +1041,18 @@ This tactical is useful with tactics such as \texttt{omega} or
 the user can avoid the explosion at time of the \texttt{Save} command
 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}
+
+When set, all lemmas generated through \texttt{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 4b2b8660c2..7c95e4d4af 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -914,6 +914,14 @@ This command turns off the normal displaying.
 \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
 This command turns the normal display on.
 
+\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
+\label{Search-Output-Name-Only}
+\index{Search Output Name Only mode}}
+This command restricts the output of search commands to identifier names; turning it on causes invocations of {\tt Search}, {\tt SearchHead}, {\tt SearchPattern}, {\tt SearchRewrite} etc. to omit types from their output, printing only identifiers.
+
+\subsection[\tt Unset Search Output Name Only.]{\tt Unset Search Output Name Only.\optindex{Search Output Name Only}}
+This command turns type display in search results back on.
+
 \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}}
 \label{SetPrintingWidth}
 This command sets which left-aligned part of the width of the screen
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f367f04c43..ddb48b0c1b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2854,7 +2854,7 @@ Additionally, it prevents a local definition such as {\tt \ident :=
 configurations containing hypotheses of the form {\tt {\ident} = $u$},
 or {\tt $u'$ = \ident} with $u'$ not a variable.
 
-The option is off by default.
+The option is on by default.
 
 \end{Variants}
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 866193ffb4..33de399c0d 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -59,6 +59,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v
     theories/Logic/FinFun.v
+    theories/Logic/PropFacts.v
   </dd>
 
   <dt> <b>Structures</b>: