coqdoc(1)

1coqdoc(1)                   General Commands Manual                  coqdoc(1)
2
3
4

NAME

6       coqdoc - A documentation tool for the Coq proof assistant
7
8
9

SYNOPSIS

11       coqdoc [ options ] files
12
13
14

DESCRIPTION

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

OPTIONS

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

NAME

SYNOPSIS

DESCRIPTION

OPTIONS

SEE ALSO