diff options
| author | tonio <tonio@pkgsrc.org> | 2007-12-01 13:05:36 +0000 |
|---|---|---|
| committer | tonio <tonio@pkgsrc.org> | 2007-12-01 13:05:36 +0000 |
| commit | 9df59f7edf90c416d476007a6dd5699c2eedf7a2 (patch) | |
| tree | 58be7b9689795793c7fa6f30f3af022bdc4e049a /lang/coq/PLIST | |
| parent | 7ef12f3aed3b451be8e85d17935bdc387ade5f86 (diff) | |
| download | pkgsrc-9df59f7edf90c416d476007a6dd5699c2eedf7a2.tar.gz | |
Update lang/coq to 8.2pl2
As camlp5 is required with ocaml 3.10, bring it as a dependency anyway,
instead of requiring ocaml 3.10
Changes include:
* Installation
- Support for compilation with ocaml 3.10 and (transitional) camlp5.
- Many bugs have been fixed (cf coq-bugs web page)
- All known failures of ROmega have been fixed. It should now be a
faithful and quicker replacement for Omega (except when nat parts
are involved). ROmega and Omega now handle <->.
- Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent) [exceptionally source of incompatibilities].
- Loading FSets/FMap used to open unwanted scopes of integer datatypes
(see bug #1347). These scopes may need to be manually opened now.
Diffstat (limited to 'lang/coq/PLIST')
| -rw-r--r-- | lang/coq/PLIST | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lang/coq/PLIST b/lang/coq/PLIST index cd61278a593..e03005158b4 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -1,4 +1,4 @@ -@comment $NetBSD: PLIST,v 1.5 2007/02/25 15:03:52 tonio Exp $ +@comment $NetBSD: PLIST,v 1.6 2007/12/01 13:05:36 tonio Exp $ bin/coq-interface bin/coq-tex bin/coq_makefile @@ -55,7 +55,9 @@ lib/coq/contrib/setoid_ring/Ring_theory.vo lib/coq/contrib/setoid_ring/ZArithRing.vo lib/coq/contrib/subtac/FixSub.vo lib/coq/contrib/subtac/FunctionalExtensionality.vo +lib/coq/contrib/subtac/Heq.vo lib/coq/contrib/subtac/Subtac.vo +lib/coq/contrib/subtac/SubtacTactics.vo lib/coq/contrib/subtac/Utils.vo lib/coq/ide/.coqide-gtk2rc lib/coq/ide/FAQ |