1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
.TH coqdoc 1
.SH NAME
coqdoc \- A documentation tool for the Coq proof assistant
.SH SYNOPSIS
.B coqdoc
[
.B options
]
.B files
.SH DESCRIPTION
.B coqdoc
is a documentation tool for the Coq proof assistant.
It creates LaTeX or HTML documents from a set of Coq files.
See the Coq reference manual for documentation (url below).
.SH OPTIONS
.SS Overall options
.TP
.BI \-h
Help. Will give you the complete list of options accepted by coqdoc.
.TP
.B \-\-html
Select a HTML output.
.TP
.B \-\-latex
Select a LATEX output.
.TP
.B \-\-dvi
Select a DVI output.
.TP
.B \-\-ps
Select a PostScript output.
.TP
.B \-\-texmacs
Select a TeXmacs output.
.TP
.B \-\-stdout
Redirect the output to stdout
.TP
.BI \-o \ file, \-\-output \ file
Redirect the output into the file
.I file.
.TP
.BI \-d \ dir, \ \-\-directory \ 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
.B \-s, \ \-\-short
Do not insert titles for the files. The default behavior is to insert
a title like ``Library Foo'' for each file.
.TP
.BI \-t \ string, \ \-\-title \ string
Set the document title.
.TP
.B \-\-body\-only
Suppress the header and trailer of the final document. Thus, you can
insert the resulting document into a larger one.
.TP
.BI \-p \ string, \ \-\-preamble \ string
Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
.TP
.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
Considers the file `file' respectively as a .v (or .g) file or a .tex file.
.TP
.BI \-\-files\-from \ file
Read file names to process in file `file' as if they were given on the
command line. Useful for program sources split in several
directories.
.TP
.B \-q, \ \-\-quiet
Be quiet. Do not print anything except errors.
.TP
.B \-h, \ \-\-help
Give a short summary of the options and exit.
.TP
.B
\-v, \ \-\-version
Print the version and exit.
.SS Index options
Default behavior is to build an index, for the HTML output only, into
index.html.
.TP
.B \-\-no\-index
Do not output the index.
.TP
.B \-\-multi\-index
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
\\tableofcontents at the beginning of the document. For a HTML output,
it builds a table of contents into toc.html.
.SS Hyperlinks options
.TP
.B \-\-glob\-from \ file
Make references using Coq globalizations from file file. (Such
globalizations are obtained with Coq option \-dump\-glob).
.TP
.B \-\-no\-externals
Do not insert links to the Coq standard library.
.TP
.BI \-\-external \ url \ libroot
Set base URL for the external library whose root prefix is libroot.
.TP
.BI \-\-coqlib_url \ url
Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
.TP
.BI \-\-coqlib \ dir
Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
.TP
.BI \-R \ dir \ coqdir
Map physical directory dir to Coq logical directory coqdir (similarly
to Coq option \-R).
.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.
.SS Contents options
.TP
.B \-g, \ \-\-gallina
Do not print proofs.
.TP
.B \-l, \ \-\-light
Light mode. Suppress proofs (as with \-g) and the following commands:
* [Recursive] Tactic Definition
* Hint / Hints
* Require
* Transparent / Opaque
* Implicit Argument / Implicits
* 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
.B \-latin1, \ \-\-latin1
Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
\-\-charset iso\-8859\-1.
.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
.BI \-\-inputenc \ string
Give a LATEX input encoding, as an option to LATEX package inputenc.
.TP
.BI \-\-charset \ string
Specify the HTML character set, to be inserted in the HTML header.
.SH SEE ALSO
.I
The Coq Reference Manual from http://coq.inria.fr/
|
