1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
The Coq development team is pleased to announce Coq version 8.0, a new
major evolution of the Coq system.
First, the logical system of Coq version 8.0 has been simplified by
removing the impredicativity of the sort Set. This allows to benefit
of the principle of description in formalisations of classical
mathematics without leading to logical inconsistencies. Impredicativity
remains available as an option for experimented users still wishing to
require this feature.
Secondly, Coq version 8.0 comes with a completely new syntax of
terms, and a revised more uniform syntax for tactics and
commands. Besides a better uniformity and a simplification of the syntax,
the purpose is to allow the use of high-level comforts, such as
implicit types in 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.
Thirdly, the standard library has been revised and simplified. There
is now only one equality "=" and one existential quantification valid
on all types. The type "R" is now in Set and the library on Z has been
re-organised. The basic notions from the initial state now have
implicit arguments.
Coq version 8.0 comes with a 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.
Coq version 8.0 brings also improved tactics (especially refined
conversion and induction tactics).
Last but not the least, Coq version 8.0 comes with a new integrated
gtk-based user interface in the style of ProofGeneral.
Please refer to the accompanying document CHANGES or the location
ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/doc/Changes.html for a full
list of changes including sources of incompatibilities.
Coq V8.0 is available in several formats from http://coq.inria.fr/
and ftp://ftp.inria.fr/INRIA/coq/V8.0/
The documentation is available in postscript, pdf and html format.
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
http://pauillac.inria.fr/mailman/listinfo/coq-club and consult the
mails archive at http://pauillac.inria.fr/pipermail/coq-club.
The Coq development team
|
