coqweb is a WEB-like tool for Coq The invocation is coqweb It creates a single LaTeX document with both documentation and Coq vernacular extracted from the given files. Documentation is inserted into Coq files as comments and thus your files will ever compile, no matter the fact you use coqweb or not. See the manual for options. COPYRIGHT ========= This program is distributed under the GNU GPL. See the enclosed file COPYING.