13 files changed, 484 insertions, 187 deletions

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7cf500400..7ffe25225 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an
 auxiliary file, produced along with the \texttt{.vo} file, the list of
 section variables used.
 
+\section{Proof blocks and error resilience}
+
+Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq
+is able to completely check a document containing errors instead of bailing
+out at the first failure.
+
+Two kind of errors are supported: errors occurring in vernacular commands and
+errors occurring in proofs.
+
+To properly recover from a failing tactic, Coq needs to recognize the structure of
+the proof in order to confine the error to a sub proof.  Proof block detection
+is performed by looking at the syntax of the proof script (i.e. also looking at indentation).
+Coq comes with four kind of proof blocks, and an ML API to add new ones.
+
+\begin{description}
+\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling}
+\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector
+\item[indent] blocks end with a tactic indented less than the previous one
+\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level
+\end{description}
+
+\subsection{Caveats}
+
+When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by
+the first error.  Error resiliency for vernacular commands can be switched off passing
+\texttt{-async-proofs-command-error-resilience off} to CoqIDE.
+
+An incorrect proof block detection can result into an incorrect error recovery and
+hence in bogus errors.  Proof block detection cannot be precise for bullets or
+any other non well parenthesized proof structure.  Error resiliency can be
+turned off or selectively activated for any set of block kind passing to
+CoqIDE one of the following options:
+\texttt{-async-proofs-tactic-error-resilience off},
+\texttt{-async-proofs-tactic-error-resilience all},
+\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}.
+Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. 
+
 \subsubsection{Automatic suggestion of proof annotations}
 
 The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
@@ -85,6 +122,9 @@ reduce the reactivity of the master process to user commands.
 To disable this feature, one can pass the \texttt{-async-proofs off} flag to
 CoqIDE.
 
+Proofs that are known to take little time to process are not delegated to a
+worker process.  The threshold can be configure with \texttt{-async-proofs-delegation-threshold}.  Default is 0.03 seconds.
+
 \section{Batch mode}
 
 When Coq is used as a batch compiler by running \texttt{coqc} or
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index a3372c296..275e1c2d5 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -4,7 +4,7 @@
 \label{CS-full}
 \index{Canonical Structures!presentation}
 
-This chapter explains the basics of Canonical Structure and how thy can be used
+\noindent This chapter explains the basics of Canonical Structure and how they can be used
 to overload notations and build a hierarchy of algebraic structures.
 The examples are taken from~\cite{CSwcu}.  We invite the interested reader
 to refer to this paper for all the details that are omitted here for brevity.
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index ee156b652..01dbcfb1c 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -3,7 +3,7 @@
 \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
 \index{Extraction}
 
-We present here the \Coq\ extraction commands, used to build certified
+\noindent We present here the \Coq\ extraction commands, used to build certified
 and relatively efficient functional programs, extracting them from
 either \Coq\ functions or \Coq\ proofs of specifications. The
 functional languages available as output are currently \ocaml{},
@@ -30,7 +30,7 @@ The next two commands are meant to be used for rapid preview of
 extraction. They both display extracted term(s) inside \Coq.
 
 \begin{description}
-\item {\tt Extraction \qualid.} ~\par
+\item {\tt Extraction \qualid{}.} ~\par
   Extraction of a constant or module in the \Coq\ toplevel.
 
 \item {\tt Recursive Extraction} \qualid$_1$ \dots\ \qualid$_n$. ~\par
@@ -40,7 +40,7 @@ extraction. They both display extracted term(s) inside \Coq.
 
 %% TODO error messages
 
-All the following commands produce real ML files. User can choose to produce
+\noindent All the following commands produce real ML files. User can choose to produce
 one monolithic file or one file per \Coq\ library. 
 
 \begin{description}
@@ -76,7 +76,7 @@ one monolithic file or one file per \Coq\ library.
   using prefixes \verb!coq_!  or \verb!Coq_!.
 \end{description}
 
-The list of globals \qualid$_i$ does not need to be
+\noindent The list of globals \qualid$_i$ does not need to be
 exhaustive: it is automatically completed into a complete and minimal
 environment. 
 
@@ -215,7 +215,7 @@ arguments. In fact, an argument can also be referred by a number
 indicating its position, starting from 1.
 \end{description}
 
-When an actual extraction takes place, an error is normally raised if the
+\noindent When an actual extraction takes place, an error is normally raised if the
 {\tt Extraction Implicit}
 declarations cannot be honored, that is if any of the implicited
 variables still occurs in the final code. This behavior can be relaxed
@@ -260,7 +260,7 @@ what ML term corresponds to a given axiom.
   be inlined everywhere instead of being declared via a let.
 \end{description}
 
-Note that the {\tt Extract Inlined Constant} command is sugar
+\noindent Note that the {\tt Extract Inlined Constant} command is sugar
 for an {\tt Extract Constant} followed by a {\tt Extraction Inline}. 
 Hence a {\tt Reset Extraction Inline} will have an effect on the
 realized and inlined axiom.
@@ -279,7 +279,7 @@ Extract Constant X => "int".
 Extract Constant x => "0".
 \end{coq_example*}
 
-Notice that in the case of type scheme axiom (i.e. whose type is an
+\noindent Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
 variables have to be given. The syntax is then:
 
@@ -287,7 +287,7 @@ variables have to be given. The syntax is then:
 \item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.}
 \end{description}
 
-The number of type variables is checked by the system. 
+\noindent The number of type variables is checked by the system. 
 
 \Example
 \begin{coq_example*}
@@ -295,7 +295,7 @@ Axiom Y : Set -> Set -> Set.
 Extract Constant Y "'a" "'b" => " 'a*'b ".
 \end{coq_example*}
 
-Realizing an axiom via {\tt Extract Constant} is only useful in the
+\noindent Realizing an axiom via {\tt Extract Constant} is only useful in the
 case of an informative axiom (of sort Type or Set). A logical axiom
 have no computational content and hence will not appears in extracted
 terms. But a warning is nonetheless issued if extraction encounters a
@@ -325,7 +325,7 @@ native boolean type instead of \Coq\ one.  The syntax is the following:
   pattern-matching of the language will be used.
 \end{description}
 
-For an inductive type with $k$ constructor, the function used to
+\noindent For an inductive type with $k$ constructor, the function used to
 emulate the match should expect $(k+1)$ arguments, first the $k$
 branches in functional form, and then the inductive element to
 destruct. For instance, the match branch \verb$| S n => foo$ gives the
@@ -365,7 +365,7 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
-If an inductive constructor or type has arity 2 and the corresponding 
+\noindent If an inductive constructor or type has arity 2 and the corresponding 
 string is enclosed by parenthesis, then the rest of the string is used
 as infix constructor or type. 
 \begin{coq_example}
@@ -373,7 +373,7 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
 \end{coq_example}
 
-As an example of translation to a non-inductive datatype, let's turn
+\noindent As an example of translation to a non-inductive datatype, let's turn
 {\tt nat} into Ocaml's {\tt int} (see caveat above):
 \begin{coq_example}
 Extract Inductive nat => int [ "0" "succ" ]
@@ -402,7 +402,7 @@ It is possible to instruct the extraction not to use particular filenames.
   Allow the extraction to use any filename.
 \end{description}
 
-For Ocaml, a typical use of these commands is
+\noindent For Ocaml, a typical use of these commands is
 {\tt Extraction Blacklist String List}.
 
 \asection{Differences between \Coq\ and ML type systems}
@@ -456,7 +456,7 @@ In Ocaml, we must cast any argument of the constructor dummy.
 
 \end{itemize}
 
-Even with those unsafe castings, you should never get error like
+\noindent Even with those unsafe castings, you should never get error like
 ``segmentation fault''. In fact even if your program may seem
 ill-typed to the Ocaml type-checker, it can't go wrong: it comes 
 from a Coq well-typed terms, so for example inductives will always 
@@ -489,7 +489,7 @@ Inductive nat : Set :=
   | S : nat -> nat.
 \end{coq_example*}
 
-This module contains a theorem {\tt eucl\_dev}, whose type is
+\noindent This module contains a theorem {\tt eucl\_dev}, whose type is
 \begin{verbatim}
 forall b:nat, b > 0 -> forall a:nat, diveucl a b
 \end{verbatim}
@@ -506,7 +506,7 @@ Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
 Recursive Extraction eucl_dev.
 \end{coq_example}
 
-The inlining of {\tt gt\_wf\_rec} and others is not
+\noindent The inlining of {\tt gt\_wf\_rec} and others is not
 mandatory. It only enhances readability of extracted code.
 You can then copy-paste the output to a file {\tt euclid.ml} or let 
 \Coq\ do it for you with the following command: 
@@ -515,7 +515,7 @@ You can then copy-paste the output to a file {\tt euclid.ml} or let
 Extraction "euclid" eucl_dev.
 \end{verbatim}
 
-Let us play the resulting program:
+\noindent Let us play the resulting program:
 
 \begin{verbatim}
 # #use "euclid.ml";;
@@ -543,7 +543,7 @@ val div : int -> int -> int * int = <fun>
 - : int * int = (11, 8)
 \end{verbatim}
 
-Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
+\noindent Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
 available via a mere {\tt Require Import ExtrOcamlIntConv} and then
 adding these functions to the list of functions to extract. This file
 {\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/}
@@ -551,7 +551,7 @@ are meant to help building concrete program via extraction.
 
 \asubsection{Extraction's horror museum}
 
-Some pathological examples of extraction are grouped in the file
+Some pathological examples of extraction are grouped in the file\\
 {\tt test-suite/success/extraction.v} of the sources of \Coq.
 
 \asubsection{Users' Contributions}
@@ -579,7 +579,7 @@ extraction test:
 \item {\tt stalmarck}
 \end{itemize}
 
-{\tt continuations} and {\tt multiplier} are a bit particular. They are
+\noindent {\tt continuations} and {\tt multiplier} are a bit particular. They are
 examples of developments where {\tt Obj.magic} are needed.  This is
 probably due to an heavy use of impredicativity. After compilation, those
 two examples run nonetheless, thanks to the correction of the
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 1efed6ef7..4daf98f87 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -4,16 +4,19 @@
 
  
 \asection{Short description of the tactics}
-\tacindex{psatz}  \tacindex{lra} 
+\tacindex{psatz}  \tacindex{lra} \tacindex{lia}  \tacindex{nia} \tacindex{nra} 
 \label{sec:psatz-hurry}
 The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to
 several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and
 {\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by
-  pre-processing the goal with the {\tt zify} tactic.}
+  pre-processing the goal with the {\tt zify} tactic.}.
+It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} 
+and reals {\tt Require Import Lra}.
 \begin{itemize}
 \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});
 \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia});
-\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra});
+\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic  (see Section~\ref{sec:lra});
+\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic  (see Section~\ref{sec:nra});
 \item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and
   {\tt n} is an optional integer limiting the proof search depth is is an
   incomplete proof procedure for non-linear arithmetic. It is based on
@@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s
 %
 There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}.
 
-\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
-\label{sec:psatz}
-The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
-In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
-Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
-refutation. 
-
-To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
-\begin{coq_eval}
-Require Import ZArith Psatz.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example*}
-Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
-\end{coq_example*}
-\begin{coq_eval}
-intro x; psatz Z 2.
-\end{coq_eval}
-Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
-cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
-(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
-bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
-x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
-Theorem~\ref{thm:psatz}, the goal is valid.
-%
-
-%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
-%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
-%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
-%
 
 \asection{{\tt lia}: a tactic for linear integer arithmetic}
 \tacindex{lia}
@@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]
 We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and
 recursively search for a proof.
 
-\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
-\tacindex{nia}
-\label{sec:nia}
-The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear  integer arithmetic.
+
+\asection{{\tt nra}: a proof procedure for non-linear arithmetic}
+\tacindex{nra}
+\label{sec:nra}
+The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic.
 %
 The tactic performs a limited amount of non-linear reasoning before running the
-linear prover of {\tt lia}.
+linear prover of {\tt lra}.
 This pre-processing does the following:
 \begin{itemize}
 \item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a
   monomial, the context is enriched with $x^2\ge 0$;
 \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$.
 \end{itemize}
-After pre-processing, the linear prover of {\tt lia} searches for a proof
+After this pre-processing, the linear prover of {\tt lra} searches for a proof
 by abstracting monomials by variables.
 
+\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic}
+\tacindex{nia}
+\label{sec:nia}
+The {\tt nia} tactic is a proof procedure for non-linear  integer arithmetic.
+%
+It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}.
+
+\asection{{\tt psatz}: a proof procedure for non-linear arithmetic}
+\label{sec:psatz}
+The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$.
+In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
+Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a
+refutation. 
+
+To illustrate the working of the tactic, consider we wish to prove the following Coq goal.
+\begin{coq_eval}
+Require Import ZArith Psatz.
+Open Scope Z_scope.
+\end{coq_eval}
+\begin{coq_example*}
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+\end{coq_example*}
+\begin{coq_eval}
+intro x; psatz Z 2.
+\end{coq_eval}
+Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the
+cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times
+(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in
+bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2,
+x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By
+Theorem~\ref{thm:psatz}, the goal is valid.
+%
+
+%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
+%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
+%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
+%
+
 
 
 %%% Local Variables: 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 3a99bfdd4..2fc1c8764 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -63,10 +63,27 @@ will be first rewritten to:
   previous one, an inequality is added in the context of the second
   branch. See for example the definition of {\tt div2} below, where the second
   branch is typed in a context where $\forall p, \_ <> S (S p)$.
-  
+
 \item Coercion. If the object being matched is coercible to an inductive
   type, the corresponding coercion will be automatically inserted. This also
   works with the previous mechanism.
+
+\end{itemize}
+
+There are options to control the generation of equalities
+and coercions.
+
+\begin{itemize}
+\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates
+  the special treatment of pattern-matching generating equalities and
+  inequalities when using \Program\ (it is on by default). All
+  pattern-matchings and let-patterns are handled using the standard
+  algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is
+  deactivated.
+\item {\tt Unset Program Generalized Coercion}\optindex{Program
+    Generalized Coercion} This deactivates the coercion of general
+  inductive types when using \Program\ (the option is on by default).
+  Coercion of subset types and pairs is still active in this case.
 \end{itemize}
 
 \subsection{Syntactic control over equalities}
@@ -261,7 +278,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-gal.tex b/doc/refman/RefMan-gal.tex
index fcccd9cb4..99eee44e0 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\binder} & ::= &   {\name} & (\ref{Binders}) \\
  & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
+ & $|$ & {\tt '} {\pattern} &\\
 & & &\\
 {\name} & ::= & {\ident} &\\
  & $|$ & {\tt \_} &\\
@@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be
 specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
 )}. There is also a notation for a sequence of binding variables
 sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt
-:}\,{\type}\,{\tt )}.
+:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote,
+e.g. {\tt '(x,y)}.
 
 Some constructions allow the binding of a variable to value. This is
 called a ``let-binder''. The entry {\binder} of the grammar accepts
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5880487f7..9378529cb 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -25,6 +25,8 @@ problems.
 \def\contexthyp{\textrm{\textsl{context\_hyp}}}
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
+\def\selector{\textrm{\textsl{selector}}}
+\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}}
 
 The syntax of the tactic language is given Figures~\ref{ltac}
 and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
@@ -78,7 +80,7 @@ For instance
 {\tt try repeat \tac$_1$ ||
   \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
 \end{quote}
-is understood as 
+is understood as
 \begin{quote}
 {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
 {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
@@ -104,6 +106,7 @@ is understood as
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
+& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -174,7 +177,7 @@ is understood as
 \\
 {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
 \\
-\tacarg & ::= & 
+\tacarg & ::= &
         {\qualid}\\
 & $|$ & {\tt ()} \\
 & $|$ & {\tt ltac :} {\atom}\\
@@ -203,7 +206,18 @@ is understood as
 & $|$ & {\integer} {\tt \,<\,} {\integer}\\
 & $|$ & {\integer} {\tt <=} {\integer}\\
 & $|$ & {\integer} {\tt \,>\,} {\integer}\\
-& $|$ & {\integer} {\tt >=} {\integer}
+& $|$ & {\integer} {\tt >=} {\integer}\\
+\\
+\selector & ::= &
+        [{\ident}]\\
+& $|$ & {\integer}\\
+& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
+          {\tt ,}\\
+\\
+\toplevelselector & ::= &
+        \selector\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language (continued)}
@@ -344,7 +358,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
     expects multiple goals, such as {\tt swap}, would act as if a single
     goal is focused.
 
-  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} 
+  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
     This variant of local tactic application is paired with a
     sequence.  In this variant, $n$ must be the number of goals
@@ -358,7 +372,58 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
 
 \end{Variants}
 
+\subsubsection[Goal selectors]{Goal selectors\label{ltac:selector}
+\tacindex{\tt :}\index{Tacticals!:@{\tt :}}}
+
+We can restrict the application of a tactic to a subset of
+the currently focused goals with:
+\begin{quote}
+  {\toplevelselector} {\tt :} {\tacexpr}
+\end{quote}
+We can also use selectors as a tactical, which allows to use them nested in
+a tactic expression, by using the keyword {\tt only}:
+\begin{quote}
+  {\tt only} {\selector} {\tt :} {\tacexpr}
+\end{quote}
+When selecting several goals, the tactic {\tacexpr} is applied globally to
+all selected goals.
+
+\begin{Variants}
+  \item{} [{\ident}] {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied locally to a goal
+    previously named by the user.
 
+  \item {\num} {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied locally to the
+    {\num}-th goal.
+
+  \item $n_1$-$m_1$, \dots, $n_k$-$m_k$ {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied globally to the subset
+    of goals described by the given ranges. You can write a single
+    $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
+
+  \item {\tt all:} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals.
+    {\tt all:} can only be used at the toplevel of a tactic expression.
+
+  \item {\tt par:} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals
+    in parallel.  The number of workers can be controlled via the
+    command line option {\tt -async-proofs-tac-j} taking as argument
+    the desired number of workers.  Limitations:  {\tt par: } only works
+    on goals containing no existential variables and {\tacexpr} must
+    either solve the goal completely or do nothing (i.e. it cannot make
+    some progress).
+    {\tt par:} can only be used at the toplevel of a tactic expression.
+
+\end{Variants}
+
+\ErrMsg \errindex{No such goal}
 
 \subsubsection[For loop]{For loop\tacindex{do}
 \index{Tacticals!do@{\tt do}}}
@@ -782,7 +847,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
 \begin{coq_example}
 Ltac f x :=
   match x with
-    context f [S ?X] => 
+    context f [S ?X] =>
     idtac X;                    (* To display the evaluation order *)
     assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
     let x:= context f[O] in assert (x=O) (* To observe the context *)
@@ -1026,7 +1091,7 @@ Reset Initial.
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
-{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
+{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
 Such auxiliary lemma is inlined in the final proof term
@@ -1041,6 +1106,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,9 +1166,9 @@ 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.
+it goes across module boundaries.
 
 If preceded by the keyword {\tt Local} the tactic definition will not
 be exported outside the current module.
@@ -1104,6 +1181,8 @@ Defined {\ltac} functions can be displayed using the command
 {\tt Print Ltac {\qualid}.}
 \end{quote}
 
+The command {\tt Print Ltac Signatures\comindex{Print Ltac Signatures}} displays a list of all user-defined tactics, with their arguments.
+
 \section{Debugging {\ltac} tactics}
 
 \subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}}
@@ -1182,6 +1261,86 @@ s: & continue current evaluation without stopping\\
 r $n$: & advance $n$ steps further\\
 r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
+
+\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
+
+It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
+
+\begin{quote}
+{\tt Set Ltac Profiling}.
+\end{quote}
+Enables the profiler
+
+\begin{quote}
+{\tt Unset Ltac Profiling}.
+\end{quote}
+Disables the profiler
+
+\begin{quote}
+{\tt Show Ltac Profile}.
+\end{quote}
+Prints the profile
+
+\begin{quote}
+{\tt Show Ltac Profile} {\qstring}.
+\end{quote}
+Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
+
+\begin{quote}
+{\tt Reset Ltac Profile}.
+\end{quote}
+Resets the profile, that is, deletes all accumulated information.  Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Require Import Coq.omega.Omega.
+
+Ltac mytauto := tauto.
+Ltac tac := intros; repeat split; omega || mytauto.
+
+Notation max x y := (x + (y - x)) (only parsing).
+\end{coq_example*}
+\begin{coq_example*}
+Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z,
+    max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z
+    /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z
+        -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A).
+Proof.
+\end{coq_example*}
+\begin{coq_example}
+  Set Ltac Profiling.
+  tac.
+\end{coq_example}
+{\let\textit\texttt% use tt mode for the output of ltacprof
+\begin{coq_example}
+  Show Ltac Profile.
+\end{coq_example}
+\begin{coq_example}
+  Show Ltac Profile "omega".
+\end{coq_example}
+}
+\begin{coq_example*}
+Abort.
+Unset Ltac Profiling.
+\end{coq_example*}
+
+\tacindex{start ltac profiling}\tacindex{stop ltac profiling}
+The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling.
+
+\begin{quote}
+{\tt start ltac profiling}.
+\end{quote}
+
+\begin{quote}
+{\tt stop ltac profiling}.
+\end{quote}
+
+You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end.
+
+Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
+
 \endinput
 
 \subsection{Permutation on closed lists}
@@ -1215,7 +1374,7 @@ Another more complex example is the problem of permutation on closed
 lists. The aim is to show that a closed list is a permutation of
 another one.  First, we define the permutation predicate as shown on
 Figure~\ref{permutpred}.
- 
+
 \begin{figure}[p]
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
@@ -1541,7 +1700,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
 \begin{coq_example*}
-Lemma isos_ex1 : 
+Lemma isos_ex1 :
   forall A B:Set, A * unit * B = B * (unit * A).
 Proof.
 intros; IsoProve.
@@ -1561,7 +1720,7 @@ Qed.
 \label{isoslem}
 \end{figure}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% End: 
+%%% End:
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index ddbe0bbb3..919e7b5cd 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
@@ -939,6 +947,14 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
+\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index aabc8a899..92107b750 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -321,6 +321,10 @@ Sometimes, a notation is expected only for the parser.
 To do so, the option {\em only parsing} is allowed in the list of modifiers of
 \texttt{Notation}.
 
+Conversely, the {\em only printing} can be used to declare
+that a notation should only be used for printing and should not declare a
+parsing rule. In particular, such notations do not modify the parser.
+
 \subsection{The \texttt{Infix} command
 \comindex{Infix}}
 
@@ -358,7 +362,7 @@ state of {\Coq}.
 Reserved Notation "x = y" (at level 70, no associativity).
 \end{coq_example}
 
-Reserving a notation is also useful for simultaneously defined an
+Reserving a notation is also useful for simultaneously defining an
 inductive type or a recursive constant and a notation for it.
 
 \Rem The notations mentioned on Figure~\ref{init-notations} are
@@ -480,6 +484,7 @@ Locate "exists _ .. _ , _".
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
   & $|$ & {\tt only parsing} \\
+  & $|$ & {\tt only printing} \\
   & $|$ & {\tt format} {\str} 
 \end{tabular}
 \end{centerframe}
@@ -584,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
   (t at level 39).
 \end{coq_example*}
 
+Recursive patterns can occur several times on the right-hand side.
+Here is an example:
+
+\begin{coq_example*}
+Notation "[> a , .. , b <]" :=
+  (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+\end{coq_example*}
+
 Notations with recursive patterns can be reserved like standard
 notations, they can also be declared within interpretation scopes (see
 section \ref{scopes}).
@@ -629,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders:
 \begin{coq_example*}
 Notation "'mylet' f x .. y :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (x closed binder, y closed binder, at level 200, right associativity).
+  (at level 200, x closed binder, y closed binder, right associativity).
+\end{coq_example*}
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+\begin{coq_example*}
+Notation ``'FUNAPP' x .. y , f'' :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
 \subsection{Summary}
@@ -860,11 +882,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type
 {\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
 recognized as an argument to be interpreted in scope {\scope}.
 
-\comindex{Bind Scope} 
-Any global reference can be bound by default to an
-interpretation scope. The command to do it is
+\comindex{Bind Scope}
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+bound to an interpretation scope. The command to do it is
 \begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
+{\tt Bind Scope} {\scope} \texttt{with} {\class}
 \end{quote}
 
 \Example
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5eb8cedd9..2da12c8d6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -42,19 +42,17 @@ language will be described in Chapter~\ref{TacticLanguage}.
 \index{tactic@{\tac}}}
 
 A tactic is applied as an ordinary command. It may be preceded by a
-goal selector: {\tt all} if the tactic is to be applied to every
-focused goal simultaneously, or a natural number $n$ if it is to be
-applied to the $n$-th goal. If no selector is specified, the default
+goal selector (see Section \ref{ltac:selector}).
+If no selector is specified, the default
 selector (see Section \ref{default-selector}) is used.
 
-\newcommand{\selector}{\nterm{selector}}
+\newcommand{\toplevelselector}{\nterm{toplevel\_selector}}
 \begin{tabular}{lcl}
-{\selector} & := & {\tt all} | {\num}\\
-{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
+{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\
  & $|$ & {\tac} {\tt .}
 \end{tabular}
-\subsection[\tt Set Default Goal Selector ``\selector''.]
-           {\tt Set Default Goal Selector ``\selector''.
+\subsection[\tt Set Default Goal Selector ``\toplevelselector''.]
+           {\tt Set Default Goal Selector ``\toplevelselector''.
             \optindex{Default Goal Selector}
             \label{default-selector}}
 After using this command, the default selector -- used when no selector
@@ -63,7 +61,9 @@ initial value is $1$, hence the tactics are, by default, applied to
 the first goal. Using {\tt Set Default Goal Selector ``all''} will
 make is so that tactics are, by default, applied to every goal
 simultaneously. Then, to apply a tactic {\tt tac} to the first goal
-only, you can write {\tt 1:tac}.
+only, you can write {\tt 1:tac}. Although more selectors are available,
+only {\tt ``all''} or a single natural number are valid default
+goal selectors.
 
 \subsection[\tt Test Default Goal Selector.]
            {\tt Test Default Goal Selector.}
@@ -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}}
 
@@ -1512,10 +1491,10 @@ the local context.
 \tacindex{contradiction}
 
 This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-hypothesis that is equivalent to {\tt False}. It permits to prune
-irrelevant cases. This tactic is a macro for the tactics sequence
-{\tt intros; elimtype False; assumption}.
+attempts to find in the current context (after all {\tt intros}) an
+hypothesis that is equivalent to an empty inductive type (e.g. {\tt
+  False}), to the negation of a singleton inductive type (e.g. {\tt
+  True} or {\tt x=x}), or two contradictory hypotheses.
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}
@@ -2301,6 +2280,21 @@ hypothesis.
 
 \end{Variants}
 
+\optindex{Structural Injection}
+
+It is possible to ensure that \texttt{injection {\term}} erases the
+original hypothesis and leaves the generated equalities in the context
+rather than putting them as antecedents of the current goal, as if
+giving \texttt{injection {\term} as} (with an empty list of names). To
+obtain this behavior, the option {\tt Set Structural Injection} must
+be activated. This option is off by default.
+
+By default, \texttt{injection} only creates new equalities between
+terms whose type is in sort \texttt{Type} or \texttt{Set}, thus
+implementing a special behavior for objects that are proofs
+of a statement in \texttt{Prop}.  This behavior can be turned off
+by setting the option \texttt{Set Keep Proof Equalities}.
+\optindex{Keep Proof Equalities}
 \subsection{\tt inversion \ident}
 \tacindex{inversion}
 
@@ -2320,6 +2314,14 @@ latter is first introduced in the local context using
 stock the lemmas whenever the same instance needs to be inverted
 several times. See Section~\ref{Derive-Inversion}.
 
+\Rem Part of the behavior of the \texttt{inversion} tactic is to generate
+equalities between expressions that appeared in the hypothesis that is
+being processed.  By default, no equalities are generated if they relate
+two proofs (i.e. equalities between terms whose type is in
+sort \texttt{Prop}).  This behavior can be turned off by using the option
+\texttt{Set Keep Proof Equalities.}
+\optindex{Keep Proof Equalities}
+
 \begin{Variants}
 \item \texttt{inversion \num}
 
@@ -2893,6 +2895,9 @@ activated, {\tt subst} also deals with the following corner cases:
     subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$
   respectively.
 
+\item The presence of a recursive equation which without the option
+  would be a cause of failure of {\tt subst}.
+  
 \item A context with cyclic dependencies as with hypotheses {\tt
   \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which
   without the option would be a cause of failure of {\tt subst}.
@@ -2905,7 +2910,7 @@ or {\tt $u'$ = \ident} with $u'$ not a variable.
 Finally, it preserves the initial order of hypotheses, which without
 the option it may break.
 
-The option is off by default.
+The option is on by default.
 
 \end{Variants}
 
@@ -3051,8 +3056,10 @@ $\beta$ (reduction of functional application), $\delta$ (unfolding of
 transparent constants, see \ref{Transparent}), $\iota$ (reduction of
 pattern-matching over a constructed term, and unfolding of {\tt fix}
 and {\tt cofix} expressions) and $\zeta$ (contraction of local
-definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota}
-or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt
+definitions), the flags are either {\tt beta}, {\tt delta},
+{\tt match}, {\tt fix}, {\tt cofix}, {\tt iota} or {\tt zeta}.
+The {\tt iota} flag is a shorthand for {\tt match}, {\tt fix} and {\tt cofix}.
+The {\tt delta} flag itself can be refined into {\tt
 delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta
 -[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the
 constants to unfold to the constants listed, and restricting in the
@@ -3300,6 +3307,16 @@ reduced to \texttt{S t}.
 
 \end{Variants}
 
+\begin{quote}
+\optindex{Refolding Reduction}
+{\tt Refolding Reduction}
+\end{quote}
+
+This option (off by default) controls the use of the refolding strategy
+of {\tt cbn} while doing reductions in unification, type inference and
+tactic applications. It can result in expensive unifications, as
+refolding currently uses a potentially exponential heuristic.
+
 \subsection{\tt unfold \qualid}
 \tacindex{unfold}
 \label{unfold}
@@ -3857,13 +3874,15 @@ Abort.
 
   This command can be used to cut the proof-search tree according to a
   regular expression matching paths to be cut. The grammar for regular
-  expressions is the following:
+  expressions is the following. Beware, there is no operator precedence
+  during parsing, one can check with \texttt{Print HintDb} to verify the
+  current cut expression:
 \[\begin{array}{lcll}
   e & ::= & \ident & \text{ hint or instance identifier } \\
-  & & \texttt{*} & \text{ any hint } \\
+  & & \texttt{\_} & \text{ any hint } \\
   & & e | e' & \text{ disjunction } \\
-  & & e ; e' & \text{ sequence } \\
-  & & ! e & \text{ Kleene star } \\
+  & & e e' & \text{ sequence } \\
+  & & e * & \text{ Kleene star } \\
   & & \texttt{emp} & \text{ empty } \\
   & & \texttt{eps} & \text{ epsilon } \\
   & & \texttt{(} e \texttt{)} & 
@@ -3881,25 +3900,33 @@ is to set the cut expression to $c | e$, the initial cut expression
 being \texttt{emp}.
 
 
-\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid}
+\item \texttt{Mode} {\tt (+ | ! | -)}$^*$ {\qualid}
 \label{HintMode}
 \comindex{Hint Mode}
 
 This sets an optional mode of use of the identifier {\qualid}.  When
 proof-search faces a goal that ends in an application of {\qualid} to
 arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the
-hints associated to qualid can be applied or not. A mode specification 
-is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is
-to be treated as an input {\tt +} or an output {\tt -} of the
-identifier. For a mode to match a list of arguments, input terms \emph{must
-not} contain existential variables, while outputs can be any term.
-Multiple modes can be declared for a single identifier, in that case 
-only one mode needs to match the arguments for the hints to be applied.
+hints associated to qualid can be applied or not. A mode specification
+is a list of $n$ {\tt +}, {\tt !} or {\tt -} items that specify if an
+argument of the identifier is to be treated as an input ({\tt +}), if
+its head only is an input ({\tt !}) or an output ({\tt -}) of the
+identifier. For a mode to match a list of arguments, input terms and
+input heads \emph{must not} contain existential variables or be
+existential variables respectively, while outputs can be any
+term. Multiple modes can be declared for a single identifier, in that
+case only one mode needs to match the arguments for the hints to be
+applied.
+
+The head of a term is understood here as the applicative head, or the
+match or projection scrutinee's head, recursively, casts being ignored.
 
 {\tt Hint Mode} is especially useful for typeclasses, when one does not
 want to support default instances and avoid ambiguity in
 general. Setting a parameter of a class as an input forces proof-search
-to be driven by that index of the class.
+to be driven by that index of the class, with {\tt !} giving more
+flexibility by allowing existentials to still appear deeper in the index
+but not at its head.
 
 \end{itemize}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index f7d07772f..9962ce996 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
 files.
 
 {\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
 
 
 \section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a08cd1475..36518e6fa 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions.
 In the monorphic case, this command declares a new global universe named
 {\ident}. It supports the polymorphic flag only in sections, meaning the
 universe quantification will be discharged on each section definition
-independently.
+independently. One cannot mix polymorphic and monomorphic declarations
+in the same section.
 
 \subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
   \comindex{Constraint}
@@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent,
 the constraint is then enforced in the global environment. Like
 \texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
 in sections only to declare constraints discharged at section closing time.
+One cannot declare a global constraint on polymorphic universes.
 
 \begin{ErrMsgs}
 \item \errindex{Undeclared universe {\ident}}.
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f..e69725838 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
 @Misc{ProofGeneral,
   author      = {David Aspinall},
   title       = {Proof General},
-  note        = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+  note        = {\url{https://proofgeneral.github.io/}}
 }
 
 @Book{CoqArt,