19 files changed, 371 insertions, 144 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 30039d4898..8f9d876cb8 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -1,4 +1,4 @@
-\achapter{Asynchronous and Parallel Proof Processing}
+\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}}
 %HEVEA\cutname{async-proofs.html}
 \aauthor{Enrico Tassi}
 
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 7ad895f9d8..376ef031db 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -280,6 +280,18 @@ Fail Check
      end).
 \end{coq_example}
 
+The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
+(off by default) removes parameters from constructors in patterns:
+\begin{coq_example}
+  Set Asymmetric Patterns.
+  Check (fun l:List nat =>
+    match l with
+    | nil => nil
+    | cons _ l' => l'
+    end)
+  Unset Asymmetric Patterns.
+\end{coq_example}
+
 \paragraph{Implicit arguments in patterns}
 By default, implicit arguments are omitted in patterns. So we write:
 
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index cab6739998..6e76d04e77 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -526,14 +526,14 @@ potentially more expensive proof-search (i.e. more useless
 backtracking).
 
 \subsection{\tt Set Typeclass Resolution After Apply}
-\optindex{Typeclasses Resolution After Apply}
+\optindex{Typeclass Resolution After Apply}
 \emph{Deprecated since 8.6}
 
 This option (off by default in Coq 8.6 and 8.5) controls the resolution
 of typeclass subgoals generated by the {\tt apply} tactic.
 
 \subsection{\tt Set Typeclass Resolution For Conversion}
-\optindex{Typeclasses Resolution For Conversion}
+\optindex{Typeclass Resolution For Conversion}
 
 This option (on by default) controls the use of typeclass resolution
 when a unification problem cannot be solved during
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 79060e6062..cff7be3e96 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -1,4 +1,4 @@
-\achapter{Extraction of programs in Objective Caml and Haskell}
+\achapter{Extraction of programs in OCaml and Haskell}
 %HEVEA\cutname{extraction.html}
 \label{Extraction}
 \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
@@ -95,12 +95,12 @@ one monolithic file or one file per \Coq\ library.
 \begin{description}
 \item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par
   All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all
-  their dependencies are extracted to a temporary Ocaml file, just as in
+  their dependencies are extracted to a temporary {\ocaml} file, just as in
   {\tt Extraction "{\em file}"}. Then this temporary file and its
-  signature are compiled with the same Ocaml compiler used to built
-  \Coq. This command succeeds only if the extraction and the Ocaml
+  signature are compiled with the same {\ocaml} compiler used to built
+  \Coq. This command succeeds only if the extraction and the {\ocaml}
   compilation succeed (and it fails if the current target language
-  of the extraction is not Ocaml).
+  of the extraction is not {\ocaml}).
 \end{description}
 
 \asection{Extraction options}
@@ -109,26 +109,26 @@ one monolithic file or one file per \Coq\ library.
 \comindex{Extraction Language}
 
 The ability to fix target language is the first and more important
-of the extraction options. Default is Ocaml.
+of the extraction options. Default is {\ocaml}.
 \begin{description}
-\item {\tt Extraction Language Ocaml}.
+\item {\tt Extraction Language OCaml}.
 \item {\tt Extraction Language Haskell}.
 \item {\tt Extraction Language Scheme}.
 \end{description}
 
 \asubsection{Inlining and optimizations}
 
-Since Objective Caml is a strict language, the extracted code has to
+Since {\ocaml} is a strict language, the extracted code has to
 be optimized in order to be efficient (for instance, when using
 induction principles we do not want to compute all the recursive calls
 but only the needed ones). So the extraction mechanism provides an
 automatic optimization routine that will be called each time the user
-want to generate Ocaml programs. The optimizations can be split in two
+want to generate {\ocaml} programs. The optimizations can be split in two
 groups: the type-preserving ones -- essentially constant inlining and
 reductions -- and the non type-preserving ones -- some function
 abstractions of dummy types are removed when it is deemed safe in order
 to have more elegant types. Therefore some constants may not appear in the
-resulting monolithic Ocaml program. In the case of modular extraction,
+resulting monolithic {\ocaml} program. In the case of modular extraction,
 even if some inlining is done, the inlined constant are nevertheless
 printed, to ensure session-independent programs.
 
@@ -367,15 +367,15 @@ As for {\tt Extract Inductive}, this command should be used with care:
 \item Extracting an inductive type to a pre-existing ML inductive type
 is quite sound. But extracting to a general type (by providing an
 ad-hoc pattern-matching) will often \emph{not} be fully rigorously
-correct.  For instance, when extracting {\tt nat} to Ocaml's {\tt
+correct.  For instance, when extracting {\tt nat} to {\ocaml}'s {\tt
 int}, it is theoretically possible to build {\tt nat} values that are
-larger than Ocaml's {\tt max\_int}. It is the user's responsibility to
+larger than {\ocaml}'s {\tt max\_int}. It is the user's responsibility to
 be sure that no overflow or other bad events occur in practice.
 
 \item Translating an inductive type to an ML type does \emph{not}
 magically improve the asymptotic complexity of functions, even if the
 ML type is an efficient representation. For instance, when extracting
-{\tt nat} to Ocaml's {\tt int}, the function {\tt mult} stays
+{\tt nat} to {\ocaml}'s {\tt int}, the function {\tt mult} stays
 quadratic. It might be interesting to associate this translation with
 some specific {\tt Extract Constant} when primitive counterparts exist.
 \end{itemize}
@@ -402,7 +402,7 @@ Extract Inductive prod => "(*)"  [ "(,)" ].
 \end{coq_example}
 
 \noindent As an example of translation to a non-inductive datatype, let's turn
-{\tt nat} into Ocaml's {\tt int} (see caveat above):
+{\tt nat} into {\ocaml}'s {\tt int} (see caveat above):
 \begin{coq_example}
 Extract Inductive nat => int [ "0" "succ" ]
  "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
@@ -417,7 +417,7 @@ directly depends from the names of the \Coq\ files. It may happen that
 these filenames are in conflict with already existing files, 
 either in the standard library of the target language or in other
 code that is meant to be linked with the extracted code. 
-For instance the module {\tt List} exists both in \Coq\ and in Ocaml.
+For instance the module {\tt List} exists both in \Coq\ and in {\ocaml}.
 It is possible to instruct the extraction not to use particular filenames.
 
 \begin{description}
@@ -430,7 +430,7 @@ It is possible to instruct the extraction not to use particular filenames.
   Allow the extraction to use any filename.
 \end{description}
 
-\noindent 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}
@@ -438,7 +438,7 @@ It is possible to instruct the extraction not to use particular filenames.
 
 Due to differences between \Coq\ and ML type systems, 
 some extracted programs are not directly typable in ML. 
-We now solve this problem (at least in Ocaml) by adding 
+We now solve this problem (at least in {\ocaml}) by adding
 when needed some unsafe casting {\tt Obj.magic}, which give
 a generic type {\tt 'a} to any term.
 
@@ -455,7 +455,7 @@ Definition dp :=
  fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y).
 \end{verbatim}
 
-In Ocaml, for instance, the direct extracted term would be
+In {\ocaml}, for instance, the direct extracted term would be
 \begin{verbatim}
 let dp x y f = Pair((f () x),(f () y))
 \end{verbatim}
@@ -480,13 +480,13 @@ Inductive anything : Type := dummy : forall A:Set, A -> anything.
 \end{verbatim}
 
 which corresponds to the definition of an ML dynamic type.
-In Ocaml, we must cast any argument of the constructor dummy.
+In {\ocaml}, we must cast any argument of the constructor dummy.
 
 \end{itemize}
 
 \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 
+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 
 have the correct number of arguments, etc. 
 
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
index 8025fbe29f..82765da6ed 100644
--- a/doc/refman/Omega.tex
+++ b/doc/refman/Omega.tex
@@ -149,6 +149,32 @@ intro; omega.
 
 % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
 
+\section{Options}
+
+\begin{quote}
+  \optindex{Stable Omega}
+  {\tt Unset Stable Omega}
+\end{quote}
+This deprecated option (on by default) is for compatibility with Coq
+pre 8.5. It resets internal name counters to make executions of
+{\tt omega} independent.
+
+\begin{quote}
+  \optindex{Omega UseLocalDefs}
+  {\tt Unset Omega UseLocalDefs}
+\end{quote}
+This option (on by default) allows {\tt omega} to use the bodies of
+local variables.
+
+\begin{quote}
+  \optindex{Omega System}
+  {\tt Set Omega System}
+  \optindex{Omega Action}
+  {\tt Set Omega Action}
+\end{quote}
+These two options (off by default) activate the printing of debug
+information.
+
 \asection{Technical data}
 \label{technical}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 5c519e46e3..a1950d136e 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -550,6 +550,60 @@ the same way as the {\Coq} kernel handles them.
 This tells if the printing matching mode is on or off. The default is
 on.
 
+\subsubsection{Factorization of clauses with same right-hand side}
+\label{SetPrintingFactorizableMatchPatterns}
+\optindex{Printing Factorizable Match Patterns}
+
+When several patterns share the same right-hand side, it is
+additionally possible to share the clauses using disjunctive patterns.
+Assuming that the printing matching mode is on, whether {\Coq}'s
+printer shall try to do this kind of factorization is governed by the
+following commands:
+
+\begin{quote}
+{\tt Set Printing Factorizable Match Patterns.}
+\end{quote}
+This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Factorizable Match Patterns.}
+\end{quote}
+This tells {\Coq}'s printer not to try to use disjunctive patterns.
+
+\begin{quote}
+{\tt Test Printing Factorizable Match Patterns.}
+\end{quote}
+This tells if the factorization of clauses with same right-hand side is
+on or off.
+
+\subsubsection{Use of a default clause}
+\label{SetPrintingAllowDefaultClause}
+\optindex{Printing Allow Default Clause}
+
+When several patterns share the same right-hand side which do not
+depend on the arguments of the patterns, yet an extra factorization is
+possible: the disjunction of patterns can be replaced with a ``{\tt
+  \_}'' default clause. Assuming that the printing matching mode and
+the factorization mode are on, whether {\Coq}'s printer shall try to
+use a default clause is governed by the following commands:
+
+\begin{quote}
+{\tt Set Printing Allow Default Clause.}
+\end{quote}
+This tells {\Coq}'s printer to use a default clause when relevant. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Allow Default Clause.}
+\end{quote}
+This tells {\Coq}'s printer not to use a default clause.
+
+\begin{quote}
+{\tt Test Printing Allow Default Clause.}
+\end{quote}
+This tells if the use of a default clause is allowed.
+
 \subsubsection{Printing of wildcard pattern
 \optindex{Printing Wildcard}}
 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 436099e74d..2d98534307 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -44,9 +44,10 @@ bottom is the status bar.
 In the script window, you may open arbitrarily many buffers to
 edit. The \emph{File} menu allows you to open files or create some,
 save them, print or export them into various formats. Among all these
-buffers, there is always one which is the current \emph{running
-  buffer}, whose name is displayed on a green background, which is the
-one where Coq commands are currently executed. 
+buffers, there is always one which is the current
+\emph{running buffer}, whose name is displayed on a background in the
+\emph{processed} color (green by default), which is the one where Coq commands
+are currently executed.
 
 Buffers may be edited as in any text editor, and classical basic
 editing commands (Copy/Paste, \ldots) are available in the \emph{Edit}
@@ -58,12 +59,13 @@ menu.
 \section{Interactive navigation into \Coq{} scripts}
 
 The running buffer is the one where navigation takes place. The
-toolbar proposes five basic commands for this. The first one,
+toolbar offers five basic navigation commands. The first one,
 represented by a down arrow icon, is for going forward executing one
 command. If that command is successful, the part of the script that
-has been executed is displayed on a green background. If that command
-fails, the error message is displayed in the message window, and the
-location of the error is emphasized by a red underline.
+has been executed is displayed on a background with the
+processed color. If that command fails, the error message is
+displayed in the message window, and the location of the error is
+emphasized by an underline in the error foreground color (red by default).
 
 On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all
 commands until the \verb|Theorem| have been already executed, and the
@@ -71,23 +73,41 @@ user tried to go forward executing \verb|Induction n|. That command
 failed because no such tactic exist (tactics are now in
 lowercase\ldots), and the wrong word is underlined. 
 
-Notice that the green part of the running buffer is not editable. If
+Notice that the processed part of the running buffer is not editable. If
 you ever want to modify something you have to go backward using the up
 arrow tool, or even better, put the cursor where you want to go back
 and use the \textsf{goto} button. Unlike with \verb|coqtop|, you
 should never use \verb|Undo| to go backward.
 
-Two additional tool buttons exist, one to go directly to the end and
-one to go back to the beginning. If you try to go to the end, or in
-general to run several commands using the \textsf{goto} button, the
-  execution will stop whenever an error is found.
+There are two additional buttons for navigation within the running buffer.
+The ``down'' button with a line goes directly to the end; the ``up'' button
+with a line goes back to the beginning. The handling of errors when using the
+go-to-the-end button depends on whether \Coq{} is running in asynchronous mode or not
+(see Chapter~\ref{Asyncprocessing}). If it is not running in that mode, execution stops
+as soon as an error is found. Otherwise, execution continues, and the
+error is marked with an underline in the error foreground color, with a background in
+the error background color (pink by default). The same characterization of
+error-handling applies when running several commands using the \textsf{goto} button.
 
 If you ever try to execute a command which happens to run during a
 long time, and would like to abort it before its
 termination, you may use the interrupt button (the white cross on a red circle).
  
-Finally, notice that these navigation buttons are also available in
-the menu, where their keyboard shortcuts are given.
+There are other buttons on the \CoqIDE{} toolbar: a button to save the running
+buffer; a button to close the current buffer (an ``X''); buttons to switch among
+buffers (left and right arrows); an ``information'' button; and a ``gears'' button.
+
+The ``information'' button is described in Section~\ref{sec:trytactics}.
+
+The ``gears'' button submits proof terms to the \Coq{} kernel for type-checking.
+When \Coq{} uses asynchronous processing (see Chapter~\ref{Asyncprocessing}), proofs may
+have been completed without kernel-checking of generated proof terms. The presence of
+unchecked proof terms is indicated by \texttt{Qed} statements
+that have a subdued \emph{being-processed} color (light blue by default),
+rather than the processed color, though their preceding proofs have the processed color.
+
+Notice that for all these buttons, except for the ``gears'' button, their operations
+are also available in the menu, where their keyboard shortcuts are given.
 
 \section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}}
 
@@ -96,8 +116,8 @@ trying to solve the current goal using simple tactics. If such a
 tactic succeeds in solving the goal, then its text is automatically
 inserted into the script. There is finally a combination of these
 tactics, called the \emph{proof wizard} which will try each of them in
-turn. This wizard is also available as a tool button (the light
-bulb).  The set of tactics tried by the wizard is customizable in
+turn. This wizard is also available as a tool button (the ``information''
+button).  The set of tactics tried by the wizard is customizable in
 the preferences.
 
 These tactics are general ones, in particular they do not refer to
@@ -132,7 +152,7 @@ arguments.
 
 \begin{figure}[t]
 \begin{center}
-%HEVEA\imgsrc[alt="coqide query window"]{coqide-queries.png}
+%HEVEA\imgsrc[alt="coqide query"]{coqide-queries.png}
 %BEGIN LATEX
 \ifpdf  % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide-queries.png}
@@ -141,27 +161,21 @@ arguments.
 \fi
 %END LATEX
 \end{center}
-\caption{\CoqIDE{}: the query window}
-\label{fig:querywindow}
+\caption{\CoqIDE{}: a Print query on a selected phrase}
+\label{fig:queryselected}
 \end{figure}
 
-
-We call \emph{query} any vernacular command that do not change the
-current state, such as \verb|Check|, \verb|Search|, etc. Those
-commands are of course useless during compilation of a file, hence
-should not be included in scripts. To run such commands without
-writing them in the script, \CoqIDE{} offers another input window
-called the \emph{query window}. This window can be displayed on
-demand, either by using the \texttt{Window} menu, or directly using
-shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{}
-the simplest way to perform a \texttt{Search} on some identifier
-is to select it using the mouse, and pressing \verb|F2|. This will
-both make appear the query window and run the \texttt{Search} in
-it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
-\verb|Check| and \verb|Print| respectively.
-Figure~\ref{fig:querywindow} displays the query window after selection
-of the word ``mult'' in the script windows, and pressing \verb|F4| to
-print its definition.
+We call \emph{query} any vernacular command that does not change the
+current state, such as \verb|Check|, \verb|Search|, etc.
+To run such commands interactively, without writing them in scripts,
+\CoqIDE{} offers a \emph{query pane}.
+The query pane can be displayed on demand by using the \texttt{View} menu,
+or using the shortcut \verb|F1|. Queries can also be performed by
+selecting a particular phrase, then choosing an item from the
+\texttt{Queries} menu. The response then appears in the message window.
+Figure~\ref{fig:queryselected} shows the result after selecting
+of the phrase \verb|Nat.mul| in the script window, and choosing \verb|Print|
+from the \texttt{Queries} menu.
 
 \section{Compilation}
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7034c56081..c4c0435c5f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -198,8 +198,6 @@ is understood as
            {\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
            {\tt =>} {\tacexpr}\\
-& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]}
-           {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
 {\it test} & ::= &
@@ -711,6 +709,55 @@ runs is displayed. Time is in seconds and is machine-dependent. The
 {\qstring} argument is optional. When provided, it is used to identify
 this particular occurrence of {\tt time}.
 
+\subsubsection{Timing a tactic that evaluates to a term\tacindex{time\_constr}\tacindex{restart\_timer}\tacindex{finish\_timing}
+\index{Tacticals!time\_constr@{\tt time\_constr}}}
+\index{Tacticals!restart\_timer@{\tt restart\_timer}}
+\index{Tacticals!finish\_timing@{\tt finish\_timing}}
+
+Tactic expressions that produce terms can be timed with the experimental tactic
+\begin{quote}
+ {\tt time\_constr} {\tacexpr}
+\end{quote}
+which evaluates {\tacexpr\tt{ ()}}
+and displays the time the tactic expression evaluated, assuming successful evaluation.
+Time is in seconds and is machine-dependent.
+
+This tactic currently does not support nesting, and will report times based on the innermost execution.
+This is due to the fact that it is implemented using the tactics
+\begin{quote}
+ {\tt restart\_timer} {\qstring}
+\end{quote}
+and
+\begin{quote}
+ {\tt finish\_timing} ({\qstring}) {\qstring}
+\end{quote}
+which (re)set and display an optionally named timer, respectively.
+The parenthesized {\qstring} argument to {\tt finish\_timing} is also
+optional, and determines the label associated with the timer for
+printing.
+
+By copying the definition of {\tt time\_constr} from the standard
+library, users can achive support for a fixed pattern of nesting by
+passing different {\qstring} parameters to {\tt restart\_timer} and
+{\tt finish\_timing} at each level of nesting.  For example:
+
+\begin{coq_example}
+Ltac time_constr1 tac :=
+  let eval_early := match goal with _ => restart_timer "(depth 1)" end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in
+  ret.
+
+Goal True.
+  let v := time_constr
+             ltac:(fun _ =>
+                     let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in
+                     let y := time_constr1 ltac:(fun _ => eval compute in x) in
+                     y) in
+  pose v.
+Abort.
+\end{coq_example}
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}}
 \index{Ltac!let rec@\texttt{let rec}}
 \index{let@\texttt{let}!in Ltac}
@@ -876,21 +923,6 @@ Goal True.
 f (3+4).
 \end{coq_example}
 
-\item \index{appcontext@\texttt{appcontext}!in pattern}
-  \optindex{Tactic Compat Context}
-For historical reasons, {\tt context} used to consider $n$-ary applications
-such as {\tt (f 1 2)} as a whole, and not as a sequence of unary
-applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail
-to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial
-application, the matched subterms would have necessarily been
-applications with exactly the same number of arguments.
-As a workaround, one could use the following variant of {\tt context}:
-\begin{quote}
-{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{quote}
-This syntax is now deprecated, as {\tt context} behaves as intended. The former
-behavior can be retrieved with the {\tt Tactic Compat Context} flag.
-
 \end{Variants}
 
 \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}
@@ -1375,10 +1407,35 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro
 {\tt stop ltac profiling}.
 \end{quote}
 
+\tacindex{reset ltac profile}\tacindex{show ltac profile}
+The following tactics behave like the corresponding vernacular commands and allow displaying and resetting the profile from tactic scripts for benchmarking purposes.
+
+\begin{quote}
+{\tt reset ltac profile}.
+\end{quote}
+
+\begin{quote}
+{\tt show ltac profile}.
+\end{quote}
+
+\begin{quote}
+{\tt show ltac profile} {\qstring}.
+\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.
 
+\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}.
+
+The following tactic behaves like {\tt idtac}, and running it compacts the heap in the
+OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}).
+
+\tacindex{optimize\_heap}
+\begin{quote}
+{\tt optimize\_heap}.
+\end{quote}
+
 \endinput
 
 \subsection{Permutation on closed lists}
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index e56c8fa7fe..b4e270e6c3 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -403,10 +403,14 @@ Fail Check B.T.
 \end{Warnings}
 
 \subsection{\tt Print Module {\ident}
-\comindex{Print Module}}
+\comindex{Print Module} \optindex{Short Module Printing}}
 
 Prints the module type and (optionally) the body of the module {\ident}.
 
+For this command and {\tt Print Module Type}, the option {\tt Short
+  Module Printing} (off by default) disables the printing of the types of fields,
+leaving only their names.
+
 \subsection{\tt Print Module Type {\ident}
 \comindex{Print Module Type}}
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3ebeba178a..1cd23c9297 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -912,6 +912,15 @@ This command turns off the use of a default timeout.
 
 This command displays whether some default timeout has be set or not.
 
+\subsection[\tt Fail \textrm{\textsl{command-or-tactic}}.]{\tt Fail \textrm{\textsl{command-or-tactic}}.\comindex{Fail}\label{Fail}}
+
+For debugging {\Coq} scripts, sometimes it is desirable to know
+whether a command or a tactic fails. If the given command or tactic
+fails, the {\tt Fail} statement succeeds, without changing the proof
+state, and in interactive mode, {\Coq} prints a message confirming the failure.
+If the command or tactic succeeds, the statement is an error, and
+{\Coq} prints a message indicating that the failure did not occur.
+
 \section{Controlling display}
 
 \subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 991c9745e9..05775bfbe5 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -499,7 +499,7 @@ Claude Marché coordinated the edition of the Reference Manual for
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
 extraction tool and module system of {\Coq}.
 
-Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando
+Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other
 contributors from Sophia-Antipolis and Nijmegen participated to the
 extension of the library.
 
@@ -659,7 +659,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an
 convenient way to write programs of given specifications, Pierre
 Corbineau extended the Mathematical Proof Language and the
 automatization tools that accompany it, Pierre Letouzey supervised and
-extended various parts the standard library, Stéphane Glondu
+extended various parts of the standard library, Stéphane Glondu
 contributed a few tactics and improvements, Jean-Marc Notin provided
 help in debugging, general maintenance and {\tt coqdoc} support,
 Vincent Siles contributed extensions of the {\tt Scheme} command and
@@ -680,7 +680,7 @@ Nicolas Tabareau made the adaptation of the interface of the old
 the interaction between Coq and its external interfaces. With Samuel
 Mimram, he also helped making Coq compatible with recent software
 tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
-improved the libraries of integers, rational, and real numbers. We
+improve the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
 particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
 team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
@@ -714,7 +714,7 @@ implementation of $\mathbb{N}$, $\mathbb{Z}$ or
 $\mathbb{Z}/n\mathbb{Z}$. 
 
 The main other evolutions of the library are due to Hugo Herbelin who
-made a revision of the sorting library (includingh a certified
+made a revision of the sorting library (including a certified
 merge-sort) and to Guillaume Melquiond who slightly revised and
 cleaned up the library of reals.
 
@@ -723,7 +723,7 @@ some efficiency issues and a more flexible construction of module
 types, Élie Soubiran brought a new model of name equivalence, the
 $\Delta$-equivalence, which respects as much as possible the names
 given by the users. He also designed with Pierre Letouzey a new
-convenient operator \verb!<+! for nesting functor application, what
+convenient operator \verb!<+! for nesting functor application, that
 provides a light notation for inheriting the properties of cascading
 modules.
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8f659ded35..6b24fdde79 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -320,10 +320,19 @@ Note that when a focused goal is proved a message is displayed
 together with a suggestion about the right bullet or {\tt \}} to
 unfocus it or focus the next one.
 
+\begin{Variants}
+
+\item {\tt {\num}: \{}\\
+This focuses on the $\num^{th}$ subgoal to prove.
+
+\end{Variants}
+
 \begin{ErrMsgs}
 \item \errindex{This proof is focused, but cannot be unfocused
     this way} You are trying to use {\tt \}} but the current subproof
   has not been fully solved.
+\item \errindex{No such goal}
+\item \errindex{Brackets only support the single numbered goal selector}
 \item see also error message about bullets below.
 \end{ErrMsgs}
 
@@ -395,6 +404,8 @@ Proof.
 
 \end{ErrMsgs}
 
+\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}}
+
 The bullet behavior can be controlled by the following commands.
 
 \begin{quote}
@@ -553,12 +564,12 @@ used to force Coq to optimize some of its internal data structures.
 This command forces Coq to shrink the data structure used to represent
 the ongoing proof.
 
-\subsection[\tt Optimize Heap.]{\tt Optimize Heap.}
+\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
 
 This command forces the OCaml runtime to perform a heap compaction.
-This is in general an expensive operation.  See:
-  \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact}
-
+This is in general an expensive operation.  See: \\
+\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
+There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 956f308512..30724759d2 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -127,8 +127,10 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
 \optindex{Boolean Equality Schemes}
 \optindex{Elimination Schemes}
 \optindex{Nonrecursive Elimination Schemes}
+\optindex{Record Elimination Schemes}
 \optindex{Case Analysis Schemes}
 \optindex{Decidable Equality Schemes}
+\optindex{Rewriting Schemes}
 \label{set-nonrecursive-elimination-schemes}
 }
 
@@ -142,6 +144,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
 declaration of the induction principles. It can be activated with the
 command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
+{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}.
 
 In addition, the {\tt Case Analysis Schemes} flag governs the generation of
 case analysis lemmas for inductive types, i.e. corresponding to the
@@ -156,6 +159,9 @@ However you have to be careful with this option since
 \Coq~ may now reject well-defined inductive types because it cannot compute
 a Boolean equality for them.
 
+The {\tt Rewriting Schemes} flag governs generation of equality
+related schemes such as congruence.
+
 \subsection{\tt Combined Scheme}
 \label{CombinedScheme}
 \comindex{Combined Scheme}
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index be199e0b24..31dabcdd4e 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -3096,10 +3096,10 @@ the tactic \ssrC{rewrite (=~ multi1)} is equivalent to
 \end{lstlisting}
 except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created.
 
-Rewriting with multirules
-is useful to implement simplification or transformation
-procedures, to be applied on terms of small to medium size. For
-instance the library \ssrL{ssrnat} provides two implementations for
+Rewriting with multirules is useful to implement simplification or
+transformation procedures, to be applied on terms of small to medium
+size. For instance, the library \ssrL{ssrnat} --- available in the
+external math-comp library --- provides two implementations for
 arithmetic operations on natural numbers: an elementary one and a tail
 recursive version, less inefficient but also less convenient for
 reasoning purposes. The library also provides one lemma per such
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 675c2bf174..66a5f107a5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3334,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code).
 
 \end{Variants}
 
+\Rem The following option makes {\tt cbv} (and its derivative {\tt
+  compute}) print information about the constants it encounters and
+the unfolding decisions it makes.
+\begin{quote}
+  \optindex{Debug Cbv}
+  {\tt Set Debug Cbv}
+\end{quote}
+
 % Obsolete? Anyway not very important message
 %\begin{ErrMsgs}
 %\item \errindex{Delta must be specified before}
@@ -3507,6 +3515,13 @@ 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.
 
+\begin{quote}
+  \optindex{Debug RAKAM}
+  {\tt Set Debug RAKAM}
+\end{quote}
+This option makes {\tt cbn} print various debugging information.
+{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine.
+
 \subsection{\tt unfold \qualid}
 \tacindex{unfold}
 \label{unfold}
@@ -3703,6 +3718,9 @@ hints of the database named {\tt core}.
   This variant is very useful for getting a better understanding of automation,
   or to know what lemmas/assumptions were used.
 
+\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics
+  it tries to solve the goal, including failing paths.
+
 \item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
   {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
   \ident$_1$ {\ldots} \ident$_n$}
@@ -3723,6 +3741,8 @@ hints of the database named {\tt core}.
 
 \item {\tt info\_trivial}
 
+\item {\tt debug trivial}
+
 \item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$
   {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
   \ident$_1$ {\ldots} \ident$_n$}
@@ -3732,6 +3752,19 @@ hints of the database named {\tt core}.
 \Rem {\tt auto} either solves completely the goal or else leaves it
 intact. \texttt{auto} and \texttt{trivial} never fail.
 
+\Rem The following options enable printing of informative or debug
+information for the {\tt auto} and {\tt trivial} tactics:
+\begin{quote}
+  \optindex{Info Auto}
+  {\tt Set Info Auto}
+  \optindex{Debug Auto}
+  {\tt Set Debug Auto}
+  \optindex{Info Trivial}
+  {\tt Set Info Trivial}
+  \optindex{Debug Trivial}
+  {\tt Set Debug Trivial}
+\end{quote}
+
 \SeeAlso Section~\ref{Hints-databases}
 
 \subsection{\tt eauto}
@@ -3768,6 +3801,14 @@ Note that {\tt ex\_intro} should be declared as a hint.
 
 \end{Variants}
 
+\Rem {\tt eauto} obeys the following options:
+\begin{quote}
+  \optindex{Info Eauto}
+  {\tt Set Info Eauto}
+  \optindex{Debug Eauto}
+  {\tt Set Debug Eauto}
+\end{quote}
+
 \SeeAlso Section~\ref{Hints-databases}
 
 \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$}
@@ -4710,6 +4751,13 @@ congruence.
     described above.
 \end{ErrMsgs}
 
+\noindent {\bf Remark: } {\tt congruence} can be made to print debug
+information by setting the following option:
+
+\begin{quote}
+\optindex{Congruence Verbose}
+{\tt Set Congruence Verbose}
+\end{quote}
 
 \section{Checking properties of terms}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c411db1001..962aa98b68 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -4,53 +4,24 @@
 The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
 
-\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}}
+\section[Using Coq as a library]{Using Coq as a library}
 
-The native-code version of \Coq\ cannot dynamically load user tactics
-using {\ocaml} code. It is possible to build a toplevel of \Coq,
-with {\ocaml} code statically linked, with the tool {\tt
-  coqmktop}.
-
-For example, one can build a native-code \Coq\ toplevel extended with a tactic
-which source is in {\tt tactic.ml} with the command
-\begin{verbatim}
-     % coqmktop -opt -o mytop.out tactic.cmx
-\end{verbatim}
-where {\tt tactic.ml} has been compiled with the native-code
-compiler {\tt ocamlopt}. This command generates an executable
-called {\tt mytop.out}. To use this executable to compile your \Coq\
-files, use {\tt coqc -image mytop.out}.
-
-A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
-which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
-
-
-\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}}
-
-One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
-order to debug your tactics with the {\ocaml} debugger.
-You need to have configured and compiled \Coq\ for debugging
-(see the file \texttt{INSTALL} included in the distribution).
-Then, you must compile the Caml modules of your tactic with the
-option \texttt{-g} (with the bytecode compiler) and build a stand-alone
-bytecode toplevel with the following command:
+In previous versions, \texttt{coqmktop} was used to build custom
+toplevels --- for example for better debugging or custom static
+linking. Nowadays, the preferred method is to use \texttt{ocamlfind}.
 
+The most basic custom toplevel is built using:
 \begin{quotation}
-\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>}
+\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
+  -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native}
 \end{quotation}
 
-
-To launch the \ocaml\ debugger with the image you need to execute it in
-an environment which correctly sets the \texttt{COQLIB} variable.
-Moreover, you have to indicate the directories in which
-\texttt{ocamldebug} should search for Caml modules.
-
-A possible solution is to use a wrapper around \texttt{ocamldebug}
-which detects the executables containing the word \texttt{coq}. In
-this case, the debugger is called with the required additional
-arguments. In other cases, the debugger is simply called without additional
-arguments. Such a wrapper can be found in the \texttt{dev/}
-subdirectory of the sources.
+For example, to statically link LTAC, you can just do:
+\begin{quotation}
+\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg
+  -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native}
+\end{quotation}
+and similarly for other plugins.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a1a6a43918..6c84a1818c 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -68,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than
 monomorphic (not universe polymorphic), so the two universes
 (in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels.
 
+When printing \texttt{pidentity}, we can see the universes it binds in
+the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set
+  Printing Universes} is on we print the ``universe context'' of
+\texttt{pidentity} consisting of the bound universes and the
+constraints they must verify (for \texttt{pidentity} there are no
+constraints).
+
 Inductive types can also be declared universes polymorphic on universes
 appearing in their parameters or fields. A typical example is given by
 monoids:
@@ -138,7 +145,7 @@ producing global universe constraints, one can use the
 \optindex{Polymorphic Inductive Cumulativity}
 
 Polymorphic inductive types, coinductive types, variants and records can be
-declared cumulative using the \texttt{Cumulative}. Alternatively,
+declared cumulative using the \texttt{Cumulative} prefix. Alternatively,
 there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
 makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
@@ -151,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} :=
 \begin{coq_example}
 Print list.
 \end{coq_example}
-When printing \texttt{list}, the part of the output of the form
-\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
-indicates the universe constraints in order to have the subtyping
-$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
-(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
-In the case of \texttt{list} there is no constraint!
-This also means that any two instances of \texttt{list} are convertible:
-$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
-furthermore their corresponding (when fully applied to convertible arguments) constructors.
+When printing \texttt{list}, the universe context indicates the
+subtyping constraints by prefixing the level names with symbols.
+
+Because inductive subtypings are only produced by comparing inductives
+to themselves with universes changed, they amount to variance
+information: each universe is either invariant, covariant or
+irrelevant (there are no contravariant subtypings in Coq),
+respectively represented by the symbols \texttt{=}, \texttt{+} and
+\texttt{*}.
+
+Here we see that \texttt{list} binds an irrelevant universe, so any
+two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever
+$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully
+applied to convertible arguments) constructors.
+
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
@@ -168,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 Print packType.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
-convertible if and only if \texttt{i $=$ j}.
+\texttt{packType} binds a covariant universe, i.e.
+$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever
+\texttt{i $\leq$ j}.
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png
index dea5626f8e..7a46ac4e68 100644
--- a/doc/refman/coqide-queries.png
+++ b/doc/refman/coqide-queries.png
diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png
index a6a0f5850e..e300401c9f 100644
--- a/doc/refman/coqide.png
+++ b/doc/refman/coqide.png