diff options
Diffstat (limited to 'ANNONCE')
| -rw-r--r-- | ANNONCE | 17 |
1 files changed, 6 insertions, 11 deletions
@@ -17,8 +17,7 @@ quantification and notations for standard arithmetical notions (e.g. +, *, <, <=) without conflicts with the rest of the syntax. A new notion of "interpretation scopes" allows also to reuse the same notations in different contexts of formalisation (e.g. +, * are valid -on nat, Z, R, types, etc). The new syntax, with explanatory examples, -is described in document ??? from the distribution. +on nat, Z, R, types, etc). Thirdly, the standard library has been revised and simplified. There is now only one equality "=" and one existential quantification valid @@ -27,9 +26,8 @@ been re-organised. The basic notions from the initial state now have implicit arguments. Coq version 8.0 comes with a smart and robust comment-preserving -automatic translator from old to new syntax. Follow the instructions -in document ??? from the distribution to update your developments from -old to new syntax. +automatic translator from old to new syntax. A translation package +with a documentation of the new syntax accompanies the distribution. Coq version 8.0 brings also a new automation tactic for first-order statements and various improvements of existing tactics. @@ -48,7 +46,9 @@ on http://www.labri.fr/~casteran/CoqArt. The sources of Coq V8.0 beta, including its integrated development environment, are available from http://coq.inria.fr/ and -ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/. +ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/. The translation +package coq-8.0beta-translator.tar.gz is available separately at +the same location. Please refer to the accompanying document CHANGES or the location ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0beta/doc/Changes.html for a @@ -57,11 +57,6 @@ full list of changes including sources of incompatibilities. The (at the time partial) documentation of Coq V8.0 is available in postscript, pdf and html format. -# Si on a le temps... - Notice that you can browse the new standard library at -http://coq.inria.fr/library-eng.html (these pages have been generated -by coqdoc). - Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs and to mail Coq-Club@pauillac.inria.fr for general questions or remarks. Note that you can now choose your personal options at |