blob: 81d2671400db1e7eb04b6c071d0c6a587fb634a4 (
plain)
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
|
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)
- a new tactic language based on a mini functional language with higher-
level pattern-matching constructs on goals (by David Delahaye)
- an improved Search facilities using patterns (by Yves Bertot)
- a "natural" syntax for real numbers (by Micaëla Mayero)
- various bug fixes
- a command to export definitions, theorems and proofs to XML to be used with
Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm)
(by Claudio Sacerdoti Coen)
Extraction and the Realizer/Program tactics are not available in Coq
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
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
Windows or MacOS.
Coq V7.0beta is available as a source package from http://coq.inria.fr
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
|
