5 files changed, 137 insertions, 11 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7cf5004003..7ffe252253 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 a3372c2965..275e1c2d55 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/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index cc7e6b53bf..ffcb371346 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -78,7 +78,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$).}
@@ -174,7 +174,7 @@ is understood as
 \\
 {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
 \\
-\tacarg & ::= & 
+\tacarg & ::= &
         {\qualid}\\
 & $|$ & {\tt ()} \\
 & $|$ & {\tt ltac :} {\atom}\\
@@ -344,7 +344,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
@@ -782,7 +782,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 +1026,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
@@ -1116,6 +1116,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}}
@@ -1194,6 +1196,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 Profile}.
+\end{quote}
+Resets the profile, that is, deletes all accumulated 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}
@@ -1227,7 +1309,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}
@@ -1553,7 +1635,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.
@@ -1573,7 +1655,7 @@ Qed.
 \label{isoslem}
 \end{figure}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% End: 
+%%% End:
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a08cd1475a..36518e6fae 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/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a12983ab84..fb45777e7f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -21,6 +21,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
+    theories/Init/Tauto.v
     theories/Init/Wf.v
     (theories/Init/Prelude.v)
   </dd>
@@ -203,6 +204,7 @@ through the <tt>Require Import</tt> command.</p>
     (theories/QArith/QArith.v)
     theories/QArith/Qreals.v
     theories/QArith/Qcanon.v
+    theories/QArith/Qcabs.v
     theories/QArith/Qround.v
     theories/QArith/QOrderedType.v
     theories/QArith/Qminmax.v