From 5939d426ac785ec063e66a302f3692b645993c56 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 28 Sep 2016 16:56:22 +0200
Subject: Add documentation for [Set Warnings] and the -w option.

---
 doc/refman/RefMan-com.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc/refman/RefMan-com.tex')

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}]\ %
 %
-- 
cgit v1.2.3


From 08c6e4c3dbe2ae851ef3097cc44618ea82717974 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 5 Dec 2016 17:26:55 -0500
Subject: the -byte option is deprecated

---
 doc/refman/RefMan-com.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index c1e552a5da..784c9ccbbf 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -26,8 +26,8 @@ run by the command {\tt coqtop}.
 They are two different binary images of \Coq: the byte-code one and
 the native-code one (if {\ocaml} provides a native-code compiler
 for your platform, which is supposed in the following). By default,
-\verb!coqc! executes the native-code version; this can be overridden
-using the \verb!-byte! option.
+\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to
+get the byte-code version.
 
 The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
-- 
cgit v1.2.3


From 2125949733b631426e955e722d6ca4e1b2eb5b60 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 5 Dec 2016 17:55:15 -0500
Subject: Change module for Coq loop

---
 doc/refman/RefMan-com.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 784c9ccbbf..bef0a1686f 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -32,7 +32,7 @@ get the byte-code version.
 The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
 the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the
-\Coq~toplevel with the command \verb!Toplevel.loop();;!.
+\Coq~toplevel with the command \verb!Coqloop.loop();;!.
 
 \section{Batch compilation ({\tt coqc})}
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
-- 
cgit v1.2.3

