Skip to content
This repository was archived by the owner on Nov 13, 2021. It is now read-only.

Files

Latest commit

author
notin
Jun 26, 2008
64a0191 · Jun 26, 2008

History

History

tools

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Jun 26, 2008
Dec 11, 1999
Dec 11, 1999
Apr 26, 2006
Apr 15, 2002
Dec 11, 1999
Jan 24, 2007
Apr 15, 2002
Jun 24, 2008
Jun 24, 2008
Mar 26, 2008
Mar 8, 2007
Jul 16, 2004
Jul 16, 2004
DESCRIPTION.

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

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 (jcfillia@lip.ens-lyon.fr)
  from caml-tex of Xavier Leroy.