diff options
| -rw-r--r-- | ANNONCE | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -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 |