diff options
| author | tonio <tonio> | 2007-02-25 15:03:52 +0000 |
|---|---|---|
| committer | tonio <tonio> | 2007-02-25 15:03:52 +0000 |
| commit | 162282bccb46d379b0ca68075469be707a2e1de5 (patch) | |
| tree | 8cab83aa4cf3e35b7cbd92a7b16df6c9b807d13c /lang/coq/distinfo | |
| parent | e4d14e6cdfbe9f8b0bc34578910d3f1b4dd27e9c (diff) | |
| download | pkgsrc-162282bccb46d379b0ca68075469be707a2e1de5.tar.gz | |
Update lang/coq to 8.1
Many changes, among them:
- Many bugs have been fixed (cf coq-bugs web page)
- changed parsing precedence of let/in and fun constructions of Ltac:
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
- New primitive "external" for communication with tool external to Coq.
- Omega now handles arbitrary precision integers.
- Haskell extraction: types of functions are now printed, better
unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
- New notation "exists! x:A, P" for unique existence.
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Few improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and
Zlt_square_simpl removed; fixed names mentioning letter O instead of
digit 0; weaken premises in Z_lt_induction).
Diffstat (limited to 'lang/coq/distinfo')
| -rw-r--r-- | lang/coq/distinfo | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lang/coq/distinfo b/lang/coq/distinfo index f0c8add20b4..46bce0304cc 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,6 +1,6 @@ -$NetBSD: distinfo,v 1.5 2006/01/27 19:22:58 tonio Exp $ +$NetBSD: distinfo,v 1.6 2007/02/25 15:03:52 tonio Exp $ -SHA1 (coq-8.0pl3.tar.gz) = b182f25b8e6591139281f7078d049aaa7f0408d8 -RMD160 (coq-8.0pl3.tar.gz) = 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7 -Size (coq-8.0pl3.tar.gz) = 2309002 bytes -SHA1 (patch-aa) = 2ef8be34bd9c77229ef9a2a6e5d04891d7e159da +SHA1 (coq-8.1.tar.gz) = 151aca5b7c919eeb39ba3c6fecec836b7953b206 +RMD160 (coq-8.1.tar.gz) = 548d2e25e7813567252f9b176f318619a780d729 +Size (coq-8.1.tar.gz) = 2977142 bytes +SHA1 (patch-aa) = 4cc1fdee8074aaa3d1af24151c2d2277522ec9bc |