12.5 Coq and LaTeX
12.5.1 Embedded Coq phrases inside LaTeX documents
When writing a documentation about a proof development, one may want to insert Coq phrases inside a LaTeX document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such Coq phrases embedded in LaTeX files: the coq-tex filter. This filter extracts Coq phrases embedded in LaTeX files, evaluates them, and insert the outcome of the evaluation after each phrase.Starting with a file file.tex containing Coq phrases, the coq-tex filter produces a file named file.v.tex with the Coq outcome.
There are options to produce the Coq parts in smaller font, italic, between horizontal rules, etc. See the man page of coq-tex for more details.
Remark. This Reference Manual and the Tutorial have been completely produced with coq-tex.
12.5.2 Pretty printing Coq listings with LaTeX
coq2latex is a tool for printing Coq listings using LaTeX :
keywords are printed in bold face, comments in italic, some tokens
are printed in a nicer way (-> becomes ®, etc.)
and indentations are kept at the beginning of lines.
Line numbers are printed in the right margin, every 10 lines.In regular mode, the command
%coq2latex file
produces a LaTeX file which is sent to the
latex command,
and the result to the dvips command. It is also possible to get the LaTeX file, DVI file or PostSCript file, on the standard output or in a file. See the man page of coq2latex for more details and options.