Skip to content

Latest commit

 

History

History
 
 

tools

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
coqdoc
coqdoc
 
 
README.coq-tex
README.coq-tex
 
 
README.emacs
README.emacs
 
 
beautify-archive
beautify-archive
 
 
check-translate
check-translate
 
 
compat5.ml
compat5.ml
 
 
compat5.mlp
compat5.mlp
 
 
compat5b.ml
compat5b.ml
 
 
compat5b.mlp
compat5b.mlp
 
 
coq-font-lock.el
coq-font-lock.el
 
 
coq-inferior.el
coq-inferior.el
 
 
coq-sl.sty
coq-sl.sty
 
 
coq_makefile.ml
coq_makefile.ml
 
 
coq_tex.ml
coq_tex.ml
 
 
coqc.ml
coqc.ml
 
 
coqdep.ml
coqdep.ml
 
 
coqdep_common.ml
coqdep_common.ml
 
 
coqdep_common.mli
coqdep_common.mli
 
 
coqdep_lexer.mli
coqdep_lexer.mli
 
 
coqdep_lexer.mll
coqdep_lexer.mll
 
 
coqmktop.ml
coqmktop.ml
 
 
coqwc.mll
coqwc.mll
 
 
coqworkmgr.ml
coqworkmgr.ml
 
 
fake_ide.ml
fake_ide.ml
 
 
gallina-db.el
gallina-db.el
 
 
gallina-syntax.el
gallina-syntax.el
 
 
gallina.el
gallina.el
 
 
gallina.ml
gallina.ml
 
 
gallina_lexer.mll
gallina_lexer.mll
 
 
mkwinapp.ml
mkwinapp.ml
 
 
ocamllibdep.mll
ocamllibdep.mll
 
 
update-require
update-require
 
 

README.coq-tex

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 ([email protected])
  from caml-tex of Xavier Leroy.