1 files changed, 18 insertions, 9 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 45230fb6e5..04a8a25c12 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -2,6 +2,7 @@
 \ttindex{coqtop}
 \ttindex{coqc}
 \ttindex{coqchk}}
+%HEVEA\cutname{commands.html}
 
 There are three \Coq~commands: 
 \begin{itemize}
@@ -106,6 +107,15 @@ The following command-line options are recognized by the commands {\tt
   recursively available from {\Coq} using absolute names (extending
   the {\dirpath} prefix) (see Section~\ref{LongNames}).
 
+  Note that only those subdirectories and files which obey the lexical
+  conventions of what is an {\ident} (see Section~\ref{lexical})
+  are taken into account. Conversely, the underlying file systems or
+  operating systems may be more restrictive than {\Coq}. While Linux's
+  ext4 file system supports any {\Coq} recursive layout
+  (within the limit of 255 bytes per file name), the default on NTFS
+  (Windows) or HFS+ (MacOS X) file systems is on the contrary to
+  disallow two files differing only in the case in the same directory.
+
   \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -R} {\em directory} {\dirpath}]\ %
@@ -204,11 +214,6 @@ The following command-line options are recognized by the commands {\tt
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ %
-
-  Enable or not special functions for Geoproof within {\CoqIDE} (default
-  is yes).
-
 \item[{\tt -color} (on|off|auto)]\ %
 
   Enable or not the coloring of output of {\tt coqtop}. Default is auto,
@@ -294,8 +299,9 @@ The following command-line options are recognized by the commands {\tt
 
 \section{Compiled libraries checker ({\tt coqchk})}
 
-The {\tt coqchk} command takes a list of library paths as argument.
-The corresponding compiled libraries (.vo files) are searched in the
+The {\tt coqchk} command takes a list of library paths as argument, described
+either by their logical name or by their physical filename, which must end in
+{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the
 path, recursively processing the libraries they depend on. The content
 of all these libraries is then type-checked. The effect of {\tt
   coqchk} is only to return with normal exit code in case of success,
@@ -325,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}]\ %