Skip to Content.
Sympa Menu

coq-club - Release of Coq V7.0 beta

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Release of Coq V7.0 beta


chronological Thread 
  • 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






Archive powered by MhonArc 2.6.16.

Top of Page