Documenting old but useful command "Print Tables".

Made a synonymous of it ("Print Options").
Also reorganized a bit the section about flags and options in reference manual.

3 files changed, 57 insertions, 16 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b517f2d2dc..8a5e8bb078 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -517,6 +517,7 @@ This tells if the non-printing of synthesizable types is on or off.
 The default is to not print synthesizable types.
 
 \subsubsection{Printing matching on irrefutable pattern
+\label{AddPrintingLet}
 \comindex{Add Printing Let {\ident}}
 \comindex{Remove Printing Let {\ident}}
 \comindex{Test Printing Let for {\ident}}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index a543561b56..4fa8e90f47 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -51,26 +51,24 @@ displays the objects defined since the beginning of this section.
 %% was introduced.
 \end{Variants}
 
-\section{Options and Flags}
-\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}}
-This command sets {\rm\sl option} to {\rm\sl value}. The original value of
-{\rm\sl option} is restored when the current module ends.
+\section{Flags, Options and Tables}
 
-\begin{Variants}
-\item {\tt Set {\rm\sl flag}.}\\
+{\Coq} configurability is based on flags (e.g. {\tt Set Printing All} in
+Section~\ref{SetPrintingAll}), options (e.g. {\tt Set Printing Width
+  {\integer}} in Section~\ref{SetPrintingWidth}), or tables (e.g. {\tt
+  Add Printing Record {\ident}}, in Section~\ref{AddPrintingLet}). The
+names of flags, options and tables are made of non-empty sequences of
+identifiers (conventionally with capital initial letter). The general
+commands handling flags, options and tables are given below.
+
+\subsection[\tt Set {\rm\sl flag}.]{\tt Set {\rm\sl flag}.\comindex{Set}}
 This command switches {\rm\sl flag} on. The original state of
 {\rm\sl flag} is restored when the current module ends.
-\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}}
-This command sets {\rm\sl option} to {\rm\sl value}. The original value of
-{\rm\sl option} is restored when the current \emph{section} ends.
+
+\begin{Variants}
 \item {\tt Local Set {\rm\sl flag}.}\\
 This command switches {\rm\sl flag} on. The original state of
 {\rm\sl flag} is restored when the current \emph{section} ends.
-\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}}
-This command sets {\rm\sl option} to {\rm\sl value}. The original value of
-{\rm\sl option} is \emph{not} restored at the end of the module. Additionally,
-if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is
-{\tt Require}-d.
 \item {\tt Global Set {\rm\sl flag}.}\\
 This command switches {\rm\sl flag} on. The original state of
 {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
@@ -93,12 +91,52 @@ if set in a file, {\rm\sl flag} is switched on when the file is
 {\tt Require}-d.
 \end{Variants}
 
+\subsection[\tt Test {\rm\sl flag}.]{\tt Test {\rm\sl flag}.\comindex{Test}}
+This command prints whether {\rm\sl flag} is on or off.
+
+\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}}
+This command sets {\rm\sl option} to {\rm\sl value}. The original value of
+{\rm\sl option} is restored when the current module ends.
+
+\begin{Variants}
+\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}}
+This command sets {\rm\sl option} to {\rm\sl value}. The original value of
+\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}}
+This command sets {\rm\sl option} to {\rm\sl value}. The original value of
+{\rm\sl option} is \emph{not} restored at the end of the module. Additionally,
+if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is
+{\tt Require}-d.
+\end{Variants}
+
+\subsection[\tt Unset {\rm\sl option}.]{\tt Unset {\rm\sl option}.\comindex{Unset}}
+This command resets {\rm\sl option} to its default value.
+
+\begin{Variants}
+\item {\tt Local Unset {\rm\sl option}.\comindex{Local Unset}}\\
+This command resets {\rm\sl option} to its default value. The original state of {\rm\sl option}
+is restored when the current \emph{section} ends.
+\item {\tt Global Unset {\rm\sl option}.\comindex{Global Unset}}\\
+This command resets {\rm\sl option} to its default value.  The original state of
+{\rm\sl option} is \emph{not} restored at the end of the module. Additionally,
+if unset in a file, {\rm\sl option} is reset to its default value when the file is
+{\tt Require}-d.
+\end{Variants}
+
 \subsection[\tt Test {\rm\sl option}.]{\tt Test {\rm\sl option}.\comindex{Test}}
 This command prints the current value of {\rm\sl option}.
 
+\subsection{Tables}
+The general commands for tables are {\tt Add {\rm\sf table} {\rm\sl
+    value}}, {\tt Remove {\rm\sf table} {\rm\sl value}}, {\tt Test
+    {\rm\sf table}}, {\tt Test {\rm\sf table} for {\rm\sl value}} and
+  {\tt Print Table {\rm\sf table}}.
+
+\subsection[\tt Print Options.]{\tt Print Options.\comindex{Print Options}}
+This commands lists all available flags, options and tables.
+
 \begin{Variants}
-\item {\tt Test {\rm\sl flag}.}\\
-This command prints whether {\rm\sl flag} is on or off.
+\item {\tt Print Tables}.\comindex{Print Tables}\\
+This is a synonymous of {\tt Print Options.}
 \end{Variants}
 
 \section{Requests to the environment}
@@ -949,6 +987,7 @@ This command turns off the normal displaying.
 This command turns the normal display on.
 
 \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}}
+\label{SetPrintingWidth}
 This command sets which left-aligned part of the width of the screen
 is used for display. 
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index be35647039..87559c9e6d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -867,6 +867,7 @@ GEXTEND Gram
          -> PrintCoercionPaths (s,t)
       | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
       | IDENT "Tables" -> PrintTables
+      | IDENT "Options" -> PrintTables (* A Synonymous to Tables *)
       | IDENT "Hint" -> PrintHintGoal
       | IDENT "Hint"; qid = smart_global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb