9 files changed, 125 insertions, 27 deletions
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-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-pro.tex b/doc/refman/RefMan-pro.tex
index 8f659ded35..1d3311edc2 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -395,6 +395,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}
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}