A new version of the Coq proof assistant is now available! You can download it from the INRIA's ftp repository: ftp://ftp.inria.fr/INRIA/logical/coq/V8.1beta.
Please be aware that this is a beta version. Its main goal is to give us some feedback from the users of Coq about the new features of Coq V8.1. If you encounter some problems using this version, please take some time to fill in our bug submission form at http://pauillac.inria.fr/coq-bugs
The file CHANGES gives a list of all improvements made in this new release. Some changes may make your old developments incompatible with Coq 8.1 (cf COMPATIBILITY).
The documentation of Coq (reference manual, tutorial, FAQ, ...) is now available along with the source code archive (in the doc directory)
The reference manual is also available online: http://coq.inria.fr/V8.1beta/refman. Some parts of the reference manual may be still outdated. We endeavour taking it up-to-date, so we advise you to check the online version of the reference manual.
The standard library of Coq V8.1 can be consulted online: http://coq.inria.fr/V8.1beta/stdlib
June 2006.