The Coq mailing list

[Andrea Asperti <asperti AT cs.unibo.it>]

COQ is "on line".

COQ standard library and main contribs are available "on line"
at http://phd.cs.unibo.it/helm/library/
The library may be consulted via a standard browser, in html mode.
HTML files are generated "on the fly" from an internal XML encoding
by means of stylesheets (passing through an intermediate MathML-content
representation).
For more information, please see http://www.cs.unibo.it/helm/

If you are interested, you may contribute to the development 
of "Coq on line" (and HELM) in several ways:

1. Coq contribs. To put your contrib on line, just send it 
   to Claudio Sacerdoti 
(sacerdot AT cs.unibo.it).
   You may either send .vo files, or a bunch of CIC.xml files, 
   exported using the new XML-facilities offered by V7. 
2. If you are interested to provide special notation for your contrib, 
   you may send us the suitable stylesheets as well. If you wish to have
   more information on the way stylesheets should be edited, please ask
   Irene Schena 
(schena AT cs.unibo.it).
3. If you are interested in mirroring "coq on line", please
   send a request to Luca Padovani 
(lpadovan AT cs.unibo.it).
4. More generally, if you wish to cooperate in the development of 
   "coq on line" and/or "helm", please send a mail to Andrea Asperti
   
(asperti AT cs.unibo.it).


                                                -- andrea asperti