From 9c0f36adac233efb1164ef88c86c78c7509d8b2c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 Nov 2017 14:57:33 +0100
Subject: Documenting the -Q flag of coqchk.

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index b4d9f60ebc..04a8a25c12 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -331,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are
 correct. {\tt coqchk} is a standalone verifier, and thus it cannot be
 tainted by such malicious code.
 
-Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
+Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
-same meaning as for {\tt coqtop}. Extra options are:
+same meaning as for {\tt coqtop}. As there is no notion of relative paths in
+object files {\tt -Q} and {\tt -R} have exactly the same meaning.
+
+Extra options are:
 \begin{description}
 \item[{\tt -norec} {\em module}]\ %
 
-- 
cgit v1.2.3