From 5eccab2a970259aee80e78e061efdd630bd97d8c Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 22 Dec 2000 19:11:25 +0000 Subject: MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1195 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ANNONCE | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/ANNONCE b/ANNONCE index 4482ee2754..81d2671400 100644 --- a/ANNONCE +++ b/ANNONCE @@ -1,7 +1,7 @@ - The LogiCal team (ex-Coq team) is releasing a new version of Coq. -Its name is V7.0beta. This new version is provided for users willing -to experiment the new features which are: + 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 primitive let-in construct - qualified names (such as Logic.f_equal) @@ -19,9 +19,9 @@ 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 -(e.g. most error messages are located). 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. +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 @@ -33,7 +33,10 @@ and ftp://ftp.inria.fr/INRIA/coq/V7. Please refer to the accompanying document Changes.dvi 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@pauillac.inria.fr for bug reports or to Coq-Club@pauillac.inria.fr for +general questions or remarks (moderated). - Jean-Christophe Filliātre and Hugo Herbelin + Jean-Christophe Filliātre and Hugo Herbelin -- cgit v1.2.3