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