summaryrefslogtreecommitdiff
path: root/man/coqchk.1
diff options
context:
space:
mode:
Diffstat (limited to 'man/coqchk.1')
-rw-r--r--man/coqchk.110
1 files changed, 7 insertions, 3 deletions
diff --git a/man/coqchk.1 b/man/coqchk.1
index 76a7cfc5..f9241c0d 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -23,7 +23,7 @@ library was not found, corrupted content, type-checking failure, etc.
.IR modules \&
is a list of modules to be checked. Modules can be referred to by a
-short or qualified name.
+short or qualified logical name, or by their filename.
.SH OPTIONS
@@ -34,13 +34,17 @@ add directory
in the include path
.TP
-.BI \-R \ dir\ coqdir
-recursively map physical
+.BI \-Q \ dir\ coqdir
+map physical
.I dir
to logical
.I coqdir
.TP
+.BI \-R \ dir\ coqdir
+synonymous for -Q
+
+.TP
.BI \-silent
makes coqchk less verbose.