Merge PR #6219: Document undocumented options

7 files changed, 101 insertions, 3 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 7ad895f9d..376ef031d 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 cab673999..6e76d04e7 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/Omega.tex b/doc/refman/Omega.tex
index 8025fbe29..82765da6e 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 e56c8fa7f..b4e270e6c 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 8f659ded3..1d3311edc 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 956f30851..30724759d 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-tac.tex b/doc/refman/RefMan-tac.tex
index 675c2bf17..66a5f107a 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}