diff options
| author | herbelin | 2006-06-09 16:41:48 +0000 |
|---|---|---|
| committer | herbelin | 2006-06-09 16:41:48 +0000 |
| commit | 7967a8d6dcaf5a1c36c3bec7ad1ac2cbeccab9db (patch) | |
| tree | d809350840be047f6198e96fcd257d26f5fb5e59 | |
| parent | e26de08521a6c9139fca655b9a237adf83920acc (diff) | |
Déplacement vers archive coq-dev-tools/distrib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8940 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ANNONCE | 49 |
1 files changed, 0 insertions, 49 deletions
diff --git a/ANNONCE b/ANNONCE deleted file mode 100644 index 2493f9cced..0000000000 --- a/ANNONCE +++ /dev/null @@ -1,49 +0,0 @@ - -It is more than two years since the last release of Coq. We're glad -to now announce the beta release of Coq version 8.1. - -The main features of Coq version 8.1 (beta) are - -- the implementation of an auxiliary algorithm for checking the - convertibility of types, specially dedicated to fast type-checking - of reflexion-based proofs, and more generally to intensive - computation - -- inductive types - - - support for recursively non uniform parameters - - support for a strong form of sort-polymorphism - -- improved tactics - - - new implementation of setoid rewrite (contributed by C. Sacerdoti Coen) - - new implementation of ring (contributed by B. Grégoire and A. Mahboubi) - - and several other new tactic features (see attached file CHANGES) - -- libraries - - - finite sets and finite maps (by J.-C. Filliâtre and P. Letouzey) - - strings (by L. Théry) - - significative extensions of the library on lists - - some other extensions (see attached file CHANGES) - - rational numbers (as a quotient over Z/Z+* -- an alternative - library based on the canonical Stern-Brocot representation is - available in the user contributions) - -- experimental features - - - new command to generate proof obligations from definitions of - programs required to meet their specification (see chapter 19 of - the reference manual) - -and many other features mentioned in the CHANGES file. - -Most of known bugs have been fixed (see coq-bugs at coq.inria.fr for details). - -Coq version 8.1 hopefully comes with only a few incompatibilities. One -purpose of this beta version is to estimate to which extent the final -version 8.1 may provide better support for compatibility. - -Coq version 8.1 is based on new Coq version 8.0. Users migrating from -Coq version 7.x and older must first translate their developments from -the old syntax using the translator provided with Coq version 8.0. |