Revbump because of ocaml 4.02, added compilation patch (already in

repository upstream) and updated package to use ocaml.mk framework.

4 files changed, 27 insertions, 14 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 4741e6cb3ac..aca975b0066 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,8 +1,9 @@
-# $NetBSD: Makefile,v 1.76 2014/10/07 16:47:28 adam Exp $
+# $NetBSD: Makefile,v 1.77 2014/10/09 22:19:01 jaapb Exp $
 #
 
 DISTNAME=	coq-8.4pl4
-PKGREVISION=	1
+PKGNAME=	${DISTNAME} # to avoid prefixing with ocaml-
+PKGREVISION=	2
 CATEGORIES=	lang math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -24,11 +25,9 @@ BUILD_TARGET=		world
 BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=3.10
 
 .include "../../mk/bsd.prefs.mk"
+.include "../../mk/ocaml.mk"
 
-.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \
-    (${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64") || \
-    (${MACHINE_ARCH} == "arm")
-PLIST.opt=	yes
+.if ${OCAML_USE_OPT_COMPILER} == "yes"
 PLIST_SUBST+=	COQIDE_TYPE="opt"
 .else
 PLIST_SUBST+=	COQIDE_TYPE="byte"
@@ -55,7 +54,7 @@ _STRIPFLAG_INSTALL=
 REPLACE_SH=	configure install.sh
 INSTALL_ENV+=	COQINSTALLPREFIX=${DESTDIR}
 
-PLIST_VARS=		coqide opt natdynlink doc
+PLIST_VARS+=		coqide natdynlink doc
 
 .include "options.mk"
 
@@ -63,6 +62,5 @@ EGDIR=		${PREFIX}/share/coq/examples
 CONF_FILES=	${EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
 
 .include "../../mk/pthread.buildlink3.mk"
-.include "../../lang/ocaml/buildlink3.mk"
 .include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index 7bcabf54c39..c4feffcd6b9 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,9 +1,9 @@
-@comment $NetBSD: PLIST,v 1.14 2013/10/30 00:21:49 minskim Exp $
+@comment $NetBSD: PLIST,v 1.15 2014/10/09 22:19:01 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
 bin/coqchk
-${PLIST.opt}bin/coqchk.opt
+${PLIST.ocaml-opt}bin/coqchk.opt
 bin/coqdep
 bin/coqdoc
 ${PLIST.coqide}bin/coqide
@@ -11,7 +11,7 @@ ${PLIST.coqide}bin/coqide.${COQIDE_TYPE}
 bin/coqmktop
 bin/coqtop
 bin/coqtop.byte
-${PLIST.opt}bin/coqtop.opt
+${PLIST.ocaml-opt}bin/coqtop.opt
 bin/coqwc
 bin/gallina
 lib/coq/config/coq_config.cmi
@@ -184,7 +184,7 @@ lib/coq/parsing/tactic_printer.cmi
 lib/coq/parsing/tok.cmi
 lib/coq/plugins/cc/cc_plugin.a
 lib/coq/plugins/cc/cc_plugin.cma
-${PLIST.opt}lib/coq/plugins/cc/cc_plugin.cmxa
+${PLIST.ocaml-opt}lib/coq/plugins/cc/cc_plugin.cmxa
 ${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
 lib/coq/plugins/cc/cc_plugin_mod.cmi
 lib/coq/plugins/cc/ccalgo.cmi
@@ -196,7 +196,7 @@ lib/coq/plugins/decl_mode/decl_interp.cmi
 lib/coq/plugins/decl_mode/decl_mode.cmi
 lib/coq/plugins/decl_mode/decl_mode_plugin.a
 lib/coq/plugins/decl_mode/decl_mode_plugin.cma
-${PLIST.opt}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxa
+${PLIST.ocaml-opt}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxa
 ${PLIST.natdynlink}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
 lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
 lib/coq/plugins/decl_mode/decl_proof_instr.cmi
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index fae00471b6a..efa95a1484a 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,6 +1,7 @@
-$NetBSD: distinfo,v 1.19 2014/05/13 14:52:28 jaapb Exp $
+$NetBSD: distinfo,v 1.20 2014/10/09 22:19:01 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 (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
new file mode 100644
index 00000000000..f3878a71b6c
--- /dev/null
+++ b/lang/coq/patches/patch-kernel_univ.ml
@@ -0,0 +1,14 @@
+$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 =