aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--man/coq-tex.16
-rw-r--r--man/coq_makefile.12
-rw-r--r--man/coqc.18
-rw-r--r--man/coqchk.14
-rw-r--r--man/coqdep.120
-rw-r--r--man/coqdoc.123
-rw-r--r--man/coqide.14
-rw-r--r--man/coqtop.110
-rw-r--r--man/coqtop.byte.14
-rw-r--r--man/coqtop.opt.14
-rw-r--r--man/coqwc.12
11 files changed, 41 insertions, 46 deletions
diff --git a/man/coq-tex.1 b/man/coq-tex.1
index 7e0a2f81e2..e4cea24c55 100644
--- a/man/coq-tex.1
+++ b/man/coq-tex.1
@@ -1,4 +1,4 @@
-.TH COQ-TEX 1 "29 March 1995"
+.TH COQ-TEX 1
.SH NAME
coq-tex \- Process Coq phrases embedded in LaTeX files
@@ -66,7 +66,7 @@ with `.v.tex' appended.
The files produced by
.B coq-tex
-can be directly processed by LaTeX.
+can be directly processed by LaTeX.
Both the Coq phrases and the toplevel output are typeset in
typewriter font.
@@ -86,7 +86,7 @@ folding is performed on the Coq input text.
Cause the file
.IR coq-image
to be executed to evaluate the Coq phrases. By default,
-this is the command
+this is the command
.IR coqtop
without specifying any path which is used to evaluate the Coq phrases.
.TP
diff --git a/man/coq_makefile.1 b/man/coq_makefile.1
index b5de6d367d..0f5912a4bb 100644
--- a/man/coq_makefile.1
+++ b/man/coq_makefile.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
.SH NAME
coq_makefile \- The Coq Proof Assistant makefile generator
diff --git a/man/coqc.1 b/man/coqc.1
index 1e597afd99..a7be343fa0 100644
--- a/man/coqc.1
+++ b/man/coqc.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
.SH NAME
coqc \- The Coq Proof Assistant compiler
@@ -19,14 +19,14 @@ is the batch compiler for the Coq Proof Assistant.
The options are basically the same as coqtop(1).
.IR file.v \&
is the vernacular file to compile.
-.IR file \&
+.IR file \&
must be formed
only with the characters `a` to `Z`, `0`-`9` or `_` and must begin
with a letter.
The compiler produces an object file
.IR file.vo \&.
-For interactive use of Coq, see
+For interactive use of Coq, see
.BR coqtop(1).
@@ -35,7 +35,7 @@ For interactive use of Coq, see
.B coqc
is a script that simply runs
.B coqtop
-with option
+with option
.B \-compile
it accepts the same options as
.B coqtop.
diff --git a/man/coqchk.1 b/man/coqchk.1
index f9241c0d47..2f9e1fd84d 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "July 7, 201"
+.TH COQ 1
.SH NAME
coqchk \- The Coq Proof Checker compiled libraries verifier
@@ -29,7 +29,7 @@ short or qualified logical name, or by their filename.
.TP
.BI \-I \ dir, \ \-\-include \ dir
-add directory
+add directory
.I dir
in the include path
diff --git a/man/coqdep.1 b/man/coqdep.1
index 0770ce88c8..b0d9606969 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "28 March 1995" "Coq tools"
+.TH COQ 1
.SH NAME
coqdep \- Compute inter-module dependencies for Coq and Caml programs
@@ -31,13 +31,13 @@ When a directory is given as argument, it is recursively looked at.
Dependencies of Coq modules are computed by looking at
.IR Require \&
commands (Require, Require Export, Require Import),
-.IR Declare \&
-.IR ML \&
+.IR Declare \&
+.IR ML \&
.IR Module \&
commands and
.IR Load \&
commands. Dependencies relative to modules from the Coq library are not
-printed except if
+printed except if
.BR \-boot \&
is given.
@@ -51,27 +51,27 @@ directives and the dot notation
.TP
.BI \-f \ file
Read filenames and options -I, -R and -Q from a _CoqProject FILE.
-.TP
+.TP
.BI \-I/\-Q/\-R \ options
Have the same effects on load path and modules names as for other
coq commands (coqtop, coqc).
-.TP
+.TP
.BI \-coqlib \ directory
Indicates where is the Coq library. The default value has been
determined at installation time, and therefore this option should not
be used under normal circumstances.
-.TP
+.TP
.BI \-exclude-dir \ dir
Skips subdirectory
.IR dir \ during
.BR -R/-Q \ search.
-.TP
+.TP
.B \-sort
Output the given file name ordered by dependencies.
.TP
.B \-vos
Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode)
-.TP
+.TP
.B \-boot
For coq developers, prints dependencies over coq library files
(omitted by default).
@@ -106,7 +106,7 @@ Consider the files (in the same directory):
where
.TP
-.BI \+
+.BI \+
D.ml contains the commands `open A', `open B' and `type t = C.t' ;
.TP
.BI \+
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 8d71a8746d..e8a58611f0 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -1,4 +1,4 @@
-.TH coqdoc 1 "April, 2006"
+.TH coqdoc 1
.SH NAME
coqdoc \- A documentation tool for the Coq proof assistant
@@ -47,12 +47,12 @@ Select a TeXmacs output.
Redirect the output to stdout
.TP
.BI \-o \ file, \-\-output \ file
-Redirect the output into the file
+Redirect the output into the file
.I file.
.TP
.BI \-d \ dir, \ \-\-directory \ dir
-Output files into directory
-.I dir
+Output files into directory
+.I dir
instead of current directory (option
\-d does not change the filename specified with option \-o, if any).
.TP
@@ -102,7 +102,7 @@ Generate one page for each category and each letter in the index,
together with a top page index.html.
.SS Table of contents option
-
+
.TP
.B \-toc, \ \-\-table\-of\-contents
Insert a table of contents. For a LATEX output, it inserts a
@@ -136,7 +136,7 @@ Set the base path where the Coq files are installed, especially style files coqd
.BI \-R \ dir \ coqdir
Map physical directory dir to Coq logical directory coqdir (similarly
to Coq option \-R).
-.B Note:
+.B Note:
option \-R only has effect on the files following it on the command
line, so you will probably need to put this option first.
@@ -155,26 +155,26 @@ Light mode. Suppress proofs (as with \-g) and the following commands:
* Require
* Transparent / Opaque
* Implicit Argument / Implicits
- * Section / Variable / Hypothesis / End
+ * Section / Variable / Hypothesis / End
The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
.SS Language options
-
+
Default behavior is to assume ASCII 7 bits input files.
-.TP
+.TP
.B \-latin1, \ \-\-latin1
Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
\-\-charset iso\-8859\-1.
-.TP
+.TP
.B \-utf8, \ \-\-utf8
Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
-.TP
+.TP
.BI \-\-inputenc \ string
Give a LATEX input encoding, as an option to LATEX package inputenc.
@@ -187,4 +187,3 @@ Specify the HTML character set, to be inserted in the HTML header.
.I
The Coq Reference Manual from http://coq.inria.fr/
-
diff --git a/man/coqide.1 b/man/coqide.1
index c1af046019..267f8a8d4b 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -1,4 +1,4 @@
-.TH COQIDE 1 "July 16, 2004"
+.TH COQIDE 1
.SH NAME
coqide \- The Coq Proof Assistant graphical interface
@@ -17,7 +17,7 @@ is a gtk graphical interface for the Coq proof assistant.
For command-line-oriented use of Coq, see
.BR coqtop (1)
-; for batch-oriented use of Coq, see
+; for batch-oriented use of Coq, see
.BR coqc (1).
diff --git a/man/coqtop.1 b/man/coqtop.1
index e799bc7748..74380f9679 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "October 11, 2006"
+.TH COQ 1
.SH NAME
coqtop \- The Coq Proof Assistant toplevel system
@@ -17,7 +17,7 @@ is the toplevel system of Coq, for interactive use.
It reads phrases on the standard input, and prints results on the
standard output.
-For batch-oriented use of Coq, see
+For batch-oriented use of Coq, see
.BR coqc(1).
@@ -29,12 +29,12 @@ Help. Will give you the complete list of options accepted by coqtop.
.TP
.BI \-I \ dir, \ \-\-include \ dir
-add directory
+add directory
.I dir
in the include path
.TP
-.BI \-R \ dir\ coqdir
+.BI \-R \ dir\ coqdir
recursively map physical
.I dir
to logical
@@ -67,7 +67,7 @@ load Coq file
(Load filename.)
.TP
-.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
+.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
load verbosely Coq file
.I filename.v
(Load Verbose filename.)
diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1
index ad1a358c32..4ef317749d 100644
--- a/man/coqtop.byte.1
+++ b/man/coqtop.byte.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
.SH NAME
coqtop.byte \- The bytecode Coq toplevel
@@ -31,5 +31,3 @@ and
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr
-
-
diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1
index 17c763da33..fc097a2ecf 100644
--- a/man/coqtop.opt.1
+++ b/man/coqtop.opt.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
.SH NAME
coqtop.opt \- The native-code Coq toplevel
@@ -31,5 +31,3 @@ and
The Coq Reference Manual.
.I
The Coq web site: http://coq.inria.fr
-
-
diff --git a/man/coqwc.1 b/man/coqwc.1
index eee37f3d1f..344b1fecc5 100644
--- a/man/coqwc.1
+++ b/man/coqwc.1
@@ -1,4 +1,4 @@
-.TH COQ 1 "16 March 2004" "Coq tools"
+.TH COQ 1
.SH NAME
coqwc \- print the number of specification, proof and comment lines in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:56:08 +0000