coq2latex1
Pretty prints coq listings
Usage
coq2latex [-]
[-latex]
[-dvi]
[-ps]
[-2e]
[-t
n]
[-c
command]
[-o
file]
[file ...]
Overview
coq2latex formats Coq sources using LaTeX(1). Keywords are pretty printed in bold face, comments in italics. Line numbers are written in the right margin.
In regular mode, coq2latex processes the input file(s) and sends the document to LaTeX(1). The resulting DVI file is sent to dvips(1).
It is possible to get the LaTeX file without any formatting (see the options below).
Options
-
-latex -
Prints the resulting LaTeX document on standard output.
-
-dvi -
Prints the resulting DVI document on standard output.
-
-ps -
Prints the resulting PostScript document on standard output.
-
-2e -
Produces a document for LaTeX2e instead of LaTeX.
--
Takes the input on standard input.
-tn-
Set the tabbing value to
n.
-ofile-
Redirect the output to the file file. May be combined with -latex, -dvi or -ps.
-ccommand-
Use the command command instead of latex (to invoke latex2e for instance).
Examples
To print two Coq files foo.v and bar.v:
example% coq2latex foo.v bar.v
To get the DVI file in foobar.dvi:
example% coq2latex -dvi -o foobar.dvi foo.v bar.v
To process the two files foo.v and bar.v as a single Coq file and to get the PostScript file on standard output:
example% cat foo.v bar.v | coq2latex - -ps
Notes
Nested comments are correctly handled.