Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

executable file 13 lines (9 sloc) 0.38 kb
1 2 3 4 5 6 7 8 9 10 11 12 13

The coq-tex filter extracts Coq phrases embedded in LaTeX files,
evaluates them, and insert the outcome of the evaluation after each

The filter is written in Perl, so you'll need Perl version 4 installed
on your machine.

USAGE. See the manual page (coq-tex.1).

AUTHOR. Jean-Christophe Filliatre (
  from caml-tex of Xavier Leroy.
Something went wrong with that request. Please try again.