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 ++++++++++++++++++-------------------
 man/coqide.1   |  8 ++------
 man/coqmktop.1 |  8 --------
 3 files changed, 20 insertions(+), 33 deletions(-)

(limited to 'man')

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
diff --git a/man/coqide.1 b/man/coqide.1
index 20379ef4..9862ebb2 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -12,11 +12,11 @@ coqide \- The Coq Proof Assistant graphical interface
 
 .SH DESCRIPTION
 
-.B coqtop
+.B coqide
 is a gtk graphical interface for the Coq proof assistant.
 
 For command-line-oriented use of Coq, see
-.BR coqide (1)
+.BR coqtop (1)
 ; for batch-oriented use of Coq, see 
 .BR coqc (1).
 
@@ -112,10 +112,6 @@ Skip loading of rcfile.
 Set the rcfile to
 .IR f .
 .TP
-.BI \-user\  u
-Use the rcfile of user
-.IR u .
-.TP
 .B \-batch
 Batch mode (exits just after arguments parsing).
 .TP
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index 1b9c9e2a..810df782 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -49,14 +49,6 @@ Link high level tactics
 Build Coq on a ocaml toplevel (incompatible with
 .BR \-opt )
 
-.TP
-.B \-searchisos
-Build a toplevel for SearchIsos
-
-.TP
-.B \-ide
-Build a toplevel for the Coq IDE
-
 .TP
 .BI \-R \ dir
 Specify recursively directories for Ocaml
-- 
cgit v1.2.3