From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 man/coqchk.1 | 37 ++++++++++++++++++-------------------
 1 file changed, 18 insertions(+), 19 deletions(-)

(limited to 'man/coqchk.1')

diff --git a/man/coqchk.1 b/man/coqchk.1
index f51861f0..76a7cfc5 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
 
@@ -41,45 +40,45 @@ recursively map physical
 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
-- 
cgit v1.2.3