fixed coqchk usage and man page + added option -coqlib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 19 deletions

diff --git a/man/coqchk.1 b/man/coqchk.1
index f51861f00..76a7cfc5d 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -1,7 +1,7 @@
-.TH COQ 1 "February 9, 2009"
+.TH COQ 1 "July 7, 201"
 
 .SH NAME
-coqchk \- The Coq Proof Assistant compiled libraries verifier
+coqchk \- The Coq Proof Checker compiled libraries verifier
 
 
 .SH SYNOPSIS
@@ -9,7 +9,7 @@ coqchk \- The Coq Proof Assistant compiled libraries verifier
 [
 .B options
 ]
-.I files-or-modules
+.I modules
 
 
 .SH DESCRIPTION
@@ -21,10 +21,9 @@ information. It returns with exit code 0 if all the requested tasks
 succeeded. A non-zero return code means that something went wrong: some
 library was not found, corrupted content, type-checking failure, etc.
 
-.IR files-or-modules \&
-is a list of modules to be checked. Modules can be referred to either
-by a filename (without the .vo suffix) or by their (possibly
-qualified) module name.
+.IR modules \&
+is a list of modules to be checked. Modules can be referred to by a
+short or qualified name.
 
 .SH OPTIONS
 
@@ -42,44 +41,44 @@ to logical
 .I coqdir
 
 .TP
-.BI \-where
-print Coq's standard library location and exit
-
-.TP
 .BI \-silent
 makes coqchk less verbose.
 
 .TP
-.BI \-admit \ file-or-module
+.BI \-admit \ module
 tag the specified module and all its dependencies as trusted, and will
 not be rechecked, unless explicitly requested by other options.
 
 .TP
-.BI \-norec \ file-or-module
+.BI \-norec \ module
 specifies that the given module shall be verified without requesting
-to check its dependencies
+to check its dependencies.
 
 .TP
 .BI \-m,\ \-\-memory
-displays a summary of the memory used by the checker
+displays a summary of the memory used by the checker.
 
 .TP
 .BI \-o,\ \-\-output\-context
 displays a summary of the logical content that have been
-verified: assumptions and usage of impredicativity
+verified: assumptions and usage of impredicativity.
 
 .TP
 .BI \-impredicative\-set
-allows the checker to verify libraries that have been compiled with
+allows the checker to accept libraries that have been compiled with
 this flag.
 
 .TP
 .BI \-v
-print Coq version and exit
+print coqchk version and exit.
+
+.TP
+.BI \-coqlib \ dir
+overrides the default location of the standard library.
 
 .TP
 .BI \-where
-print Coq's standard library location and exit
+print coqchk standard library location and exit.
 
 .TP
 .BI \-h,\ \-\-help