---
name: "coq2latex"
section: "1"
platform: "linux"
package: "coq"
version: "6.3.1-2"
release: "Debian 2.2 (Potato)"
platforms: ["linux"]
url: "https://new.carta.tech/coq2latex"
---

# coq2latex(1)

pretty prints Coq listings

## NAME

coq2latex - pretty prints Coq listings

## SYNOPSIS

**coq2latex** \[ **-** \] \[ **-latex** \] \[ **-dvi** \] \[ **-ps** \] \[ **-2e** \] \[ **-t** *n* \] \[ **-c** *command* \] \[ **-o** *file* \] \[ *file ...* \]

## DESCRIPTION

*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)](/dvips/1.md).

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.

- **-t** *n*

  Set the tabbing value to **n.**

- **-o** *file*

  Redirect the output to the file *file.* May be combined with *-latex,* *-dvi* or *-ps.*

- **-c** *command*

  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.

## BUGS

Please report any bug to **coq@pauillac.inria.fr**