Add documentation for [Set Warnings] and the -w option.

3 files changed, 20 insertions, 1 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6f85849888..c1e552a5da 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt
   available for {\tt coqc} only; it is the counterpart of {\tt
     -compile-verbose}.
 
+  \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ %
+
+  Configure the display of warnings. This option expects {\tt all}, {\tt none}
+  or a comma-separated list of warning names or categories (see
+  Section~\ref{SetWarnings}).
+
 %Mostly unused in the code
 %\item[{\tt -debug}]\ %
 %
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 919e7b5cdc..3a9db5ead2 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -914,6 +914,19 @@ This command turns off the normal displaying.
 \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
 This command turns the normal display on.
 
+\subsection[\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$).]{{\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$)}.\optindex{Warnings}}
+\label{SetWarnings}
+This command configures the display of warnings. It is experimental, and expects
+\texttt{all}, \texttt{none} or a comma-separated list of warning names or
+categories. Adding~\texttt{-} in front of a warning disables it,
+adding~\texttt{+} makes it an error. It is possible to use the special categories
+\texttt{all} and \texttt{default}, the latter containing the warnings enabled by
+default. The flags are interpreted from left to right, so in case of an overlap,
+the flags on the right have higher priority, meaning that \texttt{A,-A} is
+equivalent to \texttt{-A}.
+
 \subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
 \label{Search-Output-Name-Only}
 \index{Search Output Name Only mode}}
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index de41f7b190..2bde1dc46b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -62,7 +62,7 @@ let print_usage_channel co command =
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
 \n  -quiet                 unset display of extra information (implies -w none)\
-\n  -w (all|none)          configure display of warnings\
+\n  -w (all|none|w1,..,wn) configure display of warnings\
 \n  -color (yes|no|auto)   configure color output\
 \n\
 \n  -q                     skip loading of rcfile\