[pkgsrc/trunk]: pkgsrc/lang/coq Updated coq to version 8.4pl6. Changes from p...

[jaapb <jaapb%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/77eb80a34387
branches:  trunk
changeset: 650666:77eb80a34387
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Sat Apr 25 13:41:18 2015 +0000

description:
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

diffstat:

 lang/coq/Makefile                     |   5 ++---
 lang/coq/PLIST                        |   3 ++-
 lang/coq/distinfo                     |   9 ++++-----
 lang/coq/patches/patch-kernel_univ.ml |  14 --------------
 4 files changed, 8 insertions(+), 23 deletions(-)

diffs (65 lines):

diff -r 7e08648bd7bc -r 77eb80a34387 lang/coq/Makefile
--- a/lang/coq/Makefile Sat Apr 25 13:40:39 2015 +0000
+++ b/lang/coq/Makefile Sat Apr 25 13:41:18 2015 +0000
@@ -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 -r 7e08648bd7bc -r 77eb80a34387 lang/coq/PLIST
--- a/lang/coq/PLIST    Sat Apr 25 13:40:39 2015 +0000
+++ b/lang/coq/PLIST    Sat Apr 25 13:41:18 2015 +0000
@@ -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/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 -r 7e08648bd7bc -r 77eb80a34387 lang/coq/distinfo
--- a/lang/coq/distinfo Sat Apr 25 13:40:39 2015 +0000
+++ b/lang/coq/distinfo Sat Apr 25 13:41:18 2015 +0000
@@ -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 -r 7e08648bd7bc -r 77eb80a34387 lang/coq/patches/patch-kernel_univ.ml
--- a/lang/coq/patches/patch-kernel_univ.ml     Sat Apr 25 13:40:39 2015 +0000
+++ /dev/null   Thu Jan 01 00:00:00 1970 +0000
@@ -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 =