diff options
| author | tonio <tonio@pkgsrc.org> | 2007-02-25 15:03:52 +0000 |
|---|---|---|
| committer | tonio <tonio@pkgsrc.org> | 2007-02-25 15:03:52 +0000 |
| commit | d7c9ff8bb9ac5ccba6e301ee376d54cf71e1839e (patch) | |
| tree | 8cab83aa4cf3e35b7cbd92a7b16df6c9b807d13c /lang/coq/Makefile | |
| parent | 562875548ccb2a3cb750e535baadf3f50a5c084d (diff) | |
| download | pkgsrc-d7c9ff8bb9ac5ccba6e301ee376d54cf71e1839e.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/Makefile')
| -rw-r--r-- | lang/coq/Makefile | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 530dab2c324..553df998aea 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,10 +1,9 @@ -# $NetBSD: Makefile,v 1.15 2007/01/17 11:14:46 tonio Exp $ +# $NetBSD: Makefile,v 1.16 2007/02/25 15:03:52 tonio Exp $ # -DISTNAME= coq-8.0pl3 -PKGREVISION= 1 +DISTNAME= coq-8.1 CATEGORIES= lang math -MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/ +MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.1/ MAINTAINER= richards+netbsd@CS.Princeton.EDU HOMEPAGE= http://coq.inria.fr/ @@ -22,7 +21,7 @@ BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.09 .include "../../mk/bsd.prefs.mk" .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \ - (${MACHINE_ARCH} == "sparc") + (${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64") PLIST_SRC= ${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST .endif |