summaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
Diffstat (limited to 'man')
-rw-r--r--man/coqchk.137
-rw-r--r--man/coqide.18
-rw-r--r--man/coqmktop.18
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