This is the announcement for the release of the Coq Proof Assistant, Version 5.10.
It may be taken as usual from anonymous ftp .
For users who are already using one of the beta-test versions of V5.10, this final release has improved documentation, streamlining of tactics (Some adaptation of your scripts may be necessary because the names of inversion tactics have changed), and compressed theory files (.vo) which keep the size of the installation much smaller and are uniform across architectures. This substantial improvement necessitates however the installation of the latest release of Caml Light; see Warning below.
For users who are still using our old release V5.8, it is high time to switch to this new system, which has been completely rebuilt, authorizes mutually recursive inductive families, compiled theory modules, extensible parsers and pretty-printers, user-programmable tactics, synthesis of implicit type arguments, and many other goodies. The distribution also includes numerous new user-contributed libraries.
The current release works under most modern UNIX platforms. A specialised interface with the Centaur environment, called CTCoq, is under completion in Sophia-Antipolis and should be available soon in beta-test.
A Macintosh version will be available next Fall.
Warning: In order to install Coq V5.10 you need to install the latest release of Caml Light 0.7, available by anonymous ftp . You also need to install the Caml Light contribution `libunix'.
As always, anomaly reports to coq@pauillac.inria.fr and general questions to coq-club@pauillac.inria.fr
We apologize for possible multiple copies of this message.