-
Notifications
You must be signed in to change notification settings - Fork 640
/
ANNONCE
69 lines (55 loc) · 2.85 KB
/
ANNONCE
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
64
65
66
67
68
The Coq development team is pleased to announce the release of Coq
version 7.3. This release offers the following novelties or improvements:
- New option -dump-glob to coqtop to dump globalizations (to be used by the
new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc).
- Elimination to Set/Type from empty propositions and to Type from
"singleton" propositions now allowed (as a consequence eqT_rec and
False_rec are now automatically available).
- Tactics:
- New "Rename x into y" for renaming hypotheses.
- New "Pose x:=u" and "Pose u" to add definitions to local context.
- Tactic Definition's without arguments now allowed in Coq states.
- Inversion has been improved and Intuition simplified but not in a
fully compatible way.
- Record's now accept anonymous fields "_" (no projection is built then)
- Haskell extraction now operational.
- Extensions of [ZArith]: Zcomplements.v, Zpower.v and Zlogarithms.v
have been moved from contrib/omega to ZArith. They now include
the Zsgn function, more induction principles (Wf_Z.v and
tail of Zcomplements.v) and one more general Euclid theorem.
We would also like to thank our users for their new contributions
(all compatible with Coq V7.3):
- CongruenceClosure: Congruence Closure Decision Procedure
(Pierre Corbineau, ENS Cachan)
- MapleMode: A Maple Mode for Coq
(David Delahaye, Micaela Mayero, Chalmers University)
- Presburger: A formalization of Presburger's algorithm
(Laurent Thery, INRIA Sophia Antipolis)
- ZChinese: A proof of the Chinese Lemma (based on ZArith)
(Pierre Letouzey, LRI Orsay)
Most known bugs of version 7.2 are fixed (for the current status of
reported bugs, see http://coq.inria.fr/bin/coq-bugs).
Pcoq user interface (http://www-sop.inria.fr/lemme/pcoq) is not
ported to V7.3 yet.
Coq V7.3 is available in several formats from http://coq.inria.fr
and ftp://ftp.inria.fr/INRIA/coq/V7.3. 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.
Notice that you can browse the standard library at
http://coq.inria.fr/library-eng.html (this pages have been generated
by coqdoc).
Please refer to the accompanying document CHANGES or the location
ftp://ftp.inria.fr/INRIA/coq/V7.3/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.
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