blob: fcee480f06ae2c0835aca2dd64f973e8b56daee8 (
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
|
The Coq development team is pleased to announce the release of Coq
version 7.2. This release fixes version 7.1 known bugs and offers
the following novelties or improvements
- Extension of standard library (sorting; trigonometric, square and square
root functions; basic plane geometry; finite sums; more on continuity
and derivability; more on min and max; tail-recursive plus and mult)
- Extended tactic "Assert H := P" for forward reasoning
- Optimised extraction
- Coercions allowed in Cases patterns
- New declaration "Canonical Structure id = t : I" to help resolution of
implicit arguments in developments using Record/Structure
- New tactic "ClearBody H" to clear local definition bodies
Coq V7.2 is available in several formats from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7.2. 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.2/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.
The Coq development team
|