6 files changed, 78 insertions, 77 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 3b12f259b6..077e2f0dfb 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -198,6 +198,7 @@
 \newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
 \newcommand{\orpattern}{\nterm{or\_pattern}}
 \newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\intropatternlist}{\nterm{intro\_pattern\_list}}
 \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
 \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
 \newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
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..cc7e6b53bf 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.
@@ -1089,7 +1101,7 @@ using the syntax:
 {\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=}
 {\tacexpr}
 \end{quote}
-A previous definition of \qualid must exist in the environment.
+A previous definition of {\qualid} must exist in the environment.
 The new definition will always be used instead of the old one and
 it goes accross module boundaries.
 
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 9a365b8297..edf986392c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -802,7 +802,7 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
 
 \end{Variants}
 
-\subsection{\tt intros {\intropattern} \mbox{\dots} \intropattern}
+\subsection{\tt intros {\intropatternlist}}
 \label{intros-pattern}
 \tacindex{intros \intropattern}
 \index{Introduction patterns}
@@ -811,9 +811,11 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
 \index{Disjunctive/conjunctive introduction patterns}
 \index{Equality introduction patterns}
 
-
-This extension of the tactic {\tt intros} combines introduction of
-variables or hypotheses and case analysis. An {\em introduction pattern} is
+This extension of the tactic {\tt intros} allows to apply tactics on
+the fly on the variables or hypotheses which have been introduced. An
+{\em introduction pattern list} {\intropatternlist} is a list of
+introduction patterns possibly containing the filling introduction
+patterns {\tt *} and {\tt **}. An {\em introduction pattern} is
 either:
 \begin{itemize}
 \item a {\em naming introduction pattern}, i.e. either one of:
@@ -827,7 +829,7 @@ either:
   \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
     \begin{itemize}
     \item a disjunction of lists of patterns:
-      {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
+      {\tt [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}
     \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)}
     \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)}
       for sequence of right-associative binary constructs
@@ -844,10 +846,6 @@ either:
 \item the wildcard: {\tt \_}
 \end{itemize}
 
-Introduction patterns can be combined into lists. An {\em introduction
-  pattern list} is a list of introduction patterns possibly containing
-the filling introduction patterns {\tt *} and {\tt **}.
-
 Assuming a goal of type $Q \to P$ (non-dependent product), or
 of type $\forall x:T,~P$ (dependent product), the behavior of
 {\tt intros $p$} is defined inductively over the structure of the
@@ -860,21 +858,22 @@ introduction pattern~$p$:
 \item introduction on \texttt{\ident} behaves as described in
   Section~\ref{intro};
 \item introduction over a disjunction of list of patterns {\tt
-  [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]}
-  expects the product to be over an inductive type
-  whose number of constructors is $n$ (or more generally over a type
-  of conclusion an inductive type built from $n$ constructors,
-  e.g. {\tt C -> A\textbackslash/B} with $n=2$ since {\tt
-    A\textbackslash/B} has 2 constructors): it destructs the introduced
-  hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
-  applies on each generated subgoal the corresponding tactic;
-  \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
-  pattern is part of a sequence of patterns, then {\Coq} completes the
-  pattern so that all the arguments of the constructors of the
-  inductive type are introduced (for instance, the list of patterns
-  {\tt [$\;$|$\;$] H} applied on goal {\tt forall x:nat, x=0 -> 0=x}
-  behaves the same as the list of patterns {\tt [$\,$|$\,$?$\,$] H},
-  up to one exception explained in the Remark below);
+  [$\intropatternlist_{1}$ | \dots\ | $\intropatternlist_n$]} expects
+  the product to be over an inductive type whose number of
+  constructors is $n$ (or more generally over a type of conclusion an
+  inductive type built from $n$ constructors, e.g. {\tt C ->
+    A\textbackslash/B} with $n=2$ since {\tt A\textbackslash/B} has 2
+  constructors): it destructs the introduced hypothesis as {\tt
+    destruct} (see Section~\ref{destruct}) would and applies on each
+  generated subgoal the corresponding tactic;
+  \texttt{intros}~$\intropatternlist_i$. The introduction patterns in
+  $\intropatternlist_i$ are expected to consume no more than the
+  number of arguments of the $i^{\mbox{\scriptsize th}}$
+  constructor. If it consumes less, then {\Coq} completes the pattern
+  so that all the arguments of the constructors of the inductive type
+  are introduced (for instance, the list of patterns {\tt [$\;$|$\;$]
+    H} applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same
+  as the list of patterns {\tt [$\,$|$\,$?$\,$] H});
 \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
   $p_n$)} expects the goal to be a product over an inductive type $I$ with a
   single constructor that itself has at least $n$ arguments: it
@@ -926,19 +925,6 @@ introduction pattern~$p$:
   not any more a quantification or an implication.
 \end{itemize}
 
-Then, if $p_1$ ... $p_n$ is a list of introduction patterns possibly
-containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$}
-\begin{itemize}
-\item introduction over {\tt *} introduces all forthcoming quantified
-  variables appearing in a row;
-\item introduction over {\tt **} introduces all forthcoming quantified
-  variables or hypotheses until the goal is not any more a
-  quantification or an implication;
-\item introduction over an introduction pattern $p$ introduces the
-  forthcoming quantified variables or premise of the goal and applies
-  the introduction pattern $p$ to it.
-\end{itemize}
-
 \Example
 
 \begin{coq_example}
@@ -949,37 +935,39 @@ intros * [a | (_,c)] f.
 Abort.
 \end{coq_eval}
 
-\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
-\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
-\label{bracketing-last}
-\begin{itemize}
-\item A wildcard pattern never succeeds when applied isolated on a
-  dependent product, while it succeeds as part of a list of
-  introduction patterns if the hypotheses that depends on it are
-  erased too.
-\item A disjunctive or conjunctive pattern followed by an introduction
-  pattern forces the introduction in the context of all arguments of
-  the constructors before applying the next pattern while a terminal
-  disjunctive or conjunctive pattern does not. Here is an example
-
-\begin{coq_example}
-Goal forall n:nat, n = 0 -> n = 0.
-intros [ | ] H.
-Show 2.
-Undo.
-intros [ | ]; intros H.
-Show 2.
-\end{coq_example}
+\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
+  $p_1$;\ldots; intros $p_n$} for the following reason: If one of the
+$p_i$ is a wildcard pattern, he might succeed in the first case
+because the further hypotheses it depends in are eventually erased too
+while it might fail in the second case because of dependencies in
+hypotheses which are not yet introduced (and a fortiori not yet
+erased).
+
+\Rem In {\tt intros $\intropatternlist$}, if the last introduction
+pattern is a disjunctive or conjunctive pattern {\tt
+  [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}, the
+completion of $\intropatternlist_i$ so that all the arguments of the
+$i^{\mbox{\scriptsize th}}$ constructors of the corresponding
+inductive type are introduced can be controlled with the
+following option:
+\optindex{Bracketing Last Introduction Pattern}
 
-\end{itemize}
+\begin{quote}
+{\tt Set Bracketing Last Introduction Pattern}
+\end{quote}
 
-This later behavior can be avoided by setting the following option:
+Force completion, if needed, when the last introduction pattern is a
+disjunctive or conjunctive pattern (this is the default).
 
 \begin{quote}
-\optindex{Bracketing Last Introduction Pattern}
-{\tt Set Bracketing Last Introduction Pattern}
+{\tt Unset Bracketing Last Introduction Pattern}
 \end{quote}
 
+Deactivate completion when the last introduction pattern is a disjunctive
+or conjunctive pattern.
+
+
+
 \subsection{\tt clear \ident}
 \tacindex{clear}
 \label{clear}
@@ -1267,18 +1255,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}}
 
@@ -2890,7 +2869,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 d6b1af797f..a12983ab84 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>: