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
62
63
|
The Coq development team is pleased to release version 7.1 of Coq.
This release is a major update on version 6.3.1 and a bug-fixes update
on version 7.0.
The main features of Coq versions 7.0 and 7.1 over version 6.3.1 are
- new primitive let-in construct
- qualified names
- new high-level tactic language
- improved search facilities
- new rewriting tactic for types equipped with specific equalities
- new tactic Field to decide equalities on commutative fields
- new tactic Fourier to solve linear inequalities on reals numbers
- new tactics DiscrR, SplitRmult and SplitAbsolu dedicated to real numbers
- new tactics for induction/case analysis in "natural" style
- new extraction algorithm managing the Type level
- export of theories to XML for publishing and rendering purposes
- deep restructuration of the code (safer, simpler and more efficient)
Compared to version 7.0, the new version provides with
- port of user contributions (including new libraries for
constructive complex analysis, floating-point numbers, P-automaton
and graph theory, and formalizations of the ABR algorithm, CTL and
TCTL temporal logic, the Railroad Crossing Problem, a subset of the
C language, imperative Bresenham line drawing algorithm, imperative
Marché's minimal edition distance algorithm, Buchberger's algorithm,
RSA cryptographic algorithm, Stalmarck tautology checker algorithm,
the Fundamental Theorem of Algebra and ZFC set theory).
- new induction tactics NewDestruct and NewInduction
- new tactic Assert for forward reasoning
- known-bugs fixed
- excessive memory use mainly fixed
The Realizer/Program tactics are not available in Coq V7.1.
The Correctness command can be used instead.
Coq V7.1 is available in several formats from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7.1. We currently provide the
following versions
package for sources
rpm package for sources
rpm packages for linux
binary package for Sun-Solaris
binary version for Windows
binary version for MacOS X (Darwin)
The documentation is available in postscript, pdf and html format.
Please refer to the accompanying document CHANGES or the location
ftp://ftp.inria.fr/INRIA/coq/V7.1/doc/Changes.html for a full list of
changes including sources of incompatibilities.
Users are kindly invited to report bugs to coq-bugs@pauillac.inria.fr
and to mail Coq-Club@pauillac.inria.fr for general questions or
remarks (moderated).
The Coq development team
|
