The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Dear Coq users,

I would  like to  announce the  existence of a  tool to  document your
proof developments, coqweb.

coqweb  is inspired  by  the literate  programming  tools (web,  cweb,
noweb, etc.). You put some LaTeX documentation in the comments of your
Coq development  and a  nice document is  produced from it,  the Coq's
parts being pretty-printed. An  index is produced giving the locations
where  the  various entities  (definitions,  lemmas, inductive  types,
etc.) are introduced.

coqweb and its documentation are available at:

        http://www.lri.fr/~filliatr/coqweb/

Suggestions and bug reports are welcome.

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr