coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- To: Coq-Club AT pauillac.inria.fr
- Subject: Release of Coq V7.0 beta
- Date: Wed, 27 Dec 2000 18:46:47 +0100 (MET)
The LogiCal team (ex-Coq team) is releasing a new version of Coq
(V7.0beta). This new version is still under development and is
provided for users willing to experiment the new features which are:
- a high-level tactic language based on a small functional core with
recursors and elaborated matching operators for terms and proof
contexts (by David Delahaye)
- a command to export theories to XML to be used with Helm's publishing
and rendering tools (see http://www.cs.unibo.it/helm)
(by Claudio Sacerdoti Coen)
- a primitive let-in construct
- qualified names (such as Logic.f_equal)
- a "natural" syntax for real numbers (by Micaela Mayero)
- an improved Search facility using patterns (by Yves Bertot)
- various bug fixes
Extraction and the Realizer/Program and Correctness tactics are not
available in Coq V7.0beta.
The internals of Coq have changed a lot and this justifies the new
major version number 7 though the differences are small for end-users
The internals of Coq will continue to change significantly in the next
months and we recommend tactic developers to take contact with us for
adapting their code.
Coq V7.0beta is a minimal version. User contributions and full
documentation are not updated. No binary package is provided for
Windows or MacOS.
Coq V7.0beta is available as a source package from "http://coq.inria.fr"
and "ftp://ftp.inria.fr/INRIA/coq/V7.0".
Please refer to the accompanying document Changes.ps for a full
list of changes including sources of incompatibilities (very few).
Users are kindly invited to provide feedback on the new features by mailing
to
coq AT pauillac.inria.fr
for bug reports or to
Coq-Club AT pauillac.inria.fr
for
general questions or remarks (moderated).
Jean-Christophe Filliâtre and Hugo Herbelin
- Release of Coq V7.0 beta, Hugo Herbelin
Archive powered by MhonArc 2.6.16.