4 files changed, 25 insertions, 14 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 0a243308d5..aea2bae38d 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 d90a027295..f268d82764 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1258,18 +1258,9 @@ in the list of subgoals remaining to prove.
   introduction pattern (in particular, if {\intropattern} is {\ident},
   the tactic behaves like \texttt{assert ({\ident} :\ {\form})}).
 
-  If {\intropattern} is a disjunctive/conjunctive 
-  introduction pattern, the tactic behaves like \texttt{assert
-    {\form}} followed by a {\tt destruct} using this introduction pattern.
-
-  If {\intropattern} is a rewriting intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by a call to {\tt
-    subst} on the resulting hypothesis, if applicable, or to {\tt
-    rewrite} otherwise.
-
-  If {\intropattern} is an injection intropattern pattern, the tactic
-  behaves like \texttt{assert {\form}} followed by {\tt injection}
-  using this introduction pattern.
+  If {\intropattern} is an action introduction pattern, the tactic
+  behaves like \texttt{assert {\form}} followed by the action done by
+  this introduction pattern.
 
 \item \texttt{assert {\form} as {\intropattern} by {\tac}}
 
@@ -2863,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}