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

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 =