diff options
author | jaapb <jaapb> | 2015-04-25 13:41:18 +0000 |
---|---|---|
committer | jaapb <jaapb> | 2015-04-25 13:41:18 +0000 |
commit | 46f63a8299e51601b22bbe7f98ddaa3512cb1d16 (patch) | |
tree | 50dd87043de049e39cb47141de3e31388979f916 | |
parent | 015242f85208611f1cb9d48e92dab1a15b1091ce (diff) | |
download | pkgsrc-46f63a8299e51601b22bbe7f98ddaa3512cb1d16.tar.gz |
Updated coq to version 8.4pl6. Changes from previous version include (apart
from bugfixes):
- Coq compilation made possible with forthcoming ocaml 4.03.
- command for locating exists notation in refman changed.
- Various improvements of the Reference Manual (especially its html version)
- implicit arguments of local definitions fixed (possible
source of incompatibilities).
- New command "Print Debug GC".
- Function cannot define graph.
- Optimizing compilation of pattern matching.
- Better inference of impossible cases in pattern-matching.
- Evar leak in pattern-matching compilation
- ill-typed replacement in "change ... with ...".
- unbound evars in "change ... with ...".
- wrong return clause of a match pattern in Ltac.
- cleared local hints for autounfold.
- cleared local hints for autounfold.
- lost evars in "change ... with ...".
- supporting let-ins in constructors for vm_compute
- unfortunate typo in compare_height.
- unfortunate typos in absorption lemmas over bool.
- Full support of utf8 Greek letters (block U0370) in coqdoc
-rw-r--r-- | lang/coq/Makefile | 5 | ||||
-rw-r--r-- | lang/coq/PLIST | 3 | ||||
-rw-r--r-- | lang/coq/distinfo | 9 | ||||
-rw-r--r-- | lang/coq/patches/patch-kernel_univ.ml | 14 |
4 files changed, 8 insertions, 23 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 64b7b999221..e3caf1c4800 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,9 +1,8 @@ -# $NetBSD: Makefile,v 1.79 2015/04/06 08:17:30 adam Exp $ +# $NetBSD: Makefile,v 1.80 2015/04/25 13:41:18 jaapb Exp $ # -DISTNAME= coq-8.4pl4 +DISTNAME= coq-8.4pl6 PKGNAME= ${DISTNAME} # to avoid prefixing with ocaml- -PKGREVISION= 4 CATEGORIES= lang math MASTER_SITES= http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/ diff --git a/lang/coq/PLIST b/lang/coq/PLIST index c4feffcd6b9..164c12d6aad 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -1,4 +1,4 @@ -@comment $NetBSD: PLIST,v 1.15 2014/10/09 22:19:01 jaapb Exp $ +@comment $NetBSD: PLIST,v 1.16 2015/04/25 13:41:18 jaapb Exp $ bin/coq-tex bin/coq_makefile bin/coqc @@ -651,6 +651,7 @@ lib/coq/theories/Logic/Epsilon.vo lib/coq/theories/Logic/Eqdep.vo lib/coq/theories/Logic/EqdepFacts.vo lib/coq/theories/Logic/Eqdep_dec.vo +lib/coq/theories/Logic/ExtensionalityFacts.vo lib/coq/theories/Logic/FunctionalExtensionality.vo lib/coq/theories/Logic/Hurkens.vo lib/coq/theories/Logic/IndefiniteDescription.vo diff --git a/lang/coq/distinfo b/lang/coq/distinfo index efa95a1484a..81a0f9a2a0f 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,7 +1,6 @@ -$NetBSD: distinfo,v 1.20 2014/10/09 22:19:01 jaapb Exp $ +$NetBSD: distinfo,v 1.21 2015/04/25 13:41:18 jaapb Exp $ -SHA1 (coq-8.4pl4.tar.gz) = 4dfc3a1ae65f5c480ddc4387d21549a526183e00 -RMD160 (coq-8.4pl4.tar.gz) = 19e3fe905f5db09710b1f862f21e9b57c28f9704 -Size (coq-8.4pl4.tar.gz) = 4067355 bytes +SHA1 (coq-8.4pl6.tar.gz) = c89525295659a805661ef91da24ecfb94e226953 +RMD160 (coq-8.4pl6.tar.gz) = f57f6e5732d3977f3346dda2749f4b9628604018 +Size (coq-8.4pl6.tar.gz) = 4099815 bytes SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4 -SHA1 (patch-kernel_univ.ml) = 2208e539870d6793b807bae46e0955b5f814f3fc diff --git a/lang/coq/patches/patch-kernel_univ.ml b/lang/coq/patches/patch-kernel_univ.ml deleted file mode 100644 index f3878a71b6c..00000000000 --- a/lang/coq/patches/patch-kernel_univ.ml +++ /dev/null @@ -1,14 +0,0 @@ -$NetBSD: patch-kernel_univ.ml,v 1.1 2014/10/09 22:19:01 jaapb Exp $ - -Fix comment. ---- kernel/univ.ml.orig 2014-04-24 15:13:03.000000000 +0000 -+++ kernel/univ.ml -@@ -226,7 +226,7 @@ let reprleq g arcu = - - - (* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *) --(* between u v = {w|u<=w<=v, w canonical} *) -+(* between u v = { w | u<=w<=v, w canonical} *) - (* between is the most costly operation *) - - let between g arcu arcv = |