3 files changed, 20 insertions, 33 deletions
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
 
@@ -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
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
@@ -50,14 +50,6 @@ 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