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.

5 files changed, 42 insertions, 16 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 040683823c9..f6f8b3ed7d1 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,10 +1,9 @@
-# $NetBSD: Makefile,v 1.17 2007/09/21 13:03:56 wiz Exp $
+# $NetBSD: Makefile,v 1.18 2007/12/01 13:05:36 tonio Exp $
 #
 
-DISTNAME=	coq-8.1
-PKGREVISION=	1
+DISTNAME=	coq-8.1pl2
 CATEGORIES=	lang math
-MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V8.1/
+MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V8.1pl2/
 
 MAINTAINER=	richards+netbsd@CS.Princeton.EDU
 HOMEPAGE=	http://coq.inria.fr/
@@ -47,4 +46,5 @@ PLIST_SUBST+=	WITH_IDE='@comment '
 
 .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 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
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 46bce0304cc..b7ef051cad8 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,6 +1,7 @@
-$NetBSD: distinfo,v 1.6 2007/02/25 15:03:52 tonio Exp $
+$NetBSD: distinfo,v 1.7 2007/12/01 13:05:36 tonio Exp $
 
-SHA1 (coq-8.1.tar.gz) = 151aca5b7c919eeb39ba3c6fecec836b7953b206
-RMD160 (coq-8.1.tar.gz) = 548d2e25e7813567252f9b176f318619a780d729
-Size (coq-8.1.tar.gz) = 2977142 bytes
-SHA1 (patch-aa) = 4cc1fdee8074aaa3d1af24151c2d2277522ec9bc
+SHA1 (coq-8.1pl2.tar.gz) = 33ab31abffe42559a5c8341b66a0520805337526
+RMD160 (coq-8.1pl2.tar.gz) = e45451fdd41b1f979febcfb2c0dbd19a39d09256
+Size (coq-8.1pl2.tar.gz) = 2997185 bytes
+SHA1 (patch-aa) = 4a518e52aea4a2e239754b6a8123b9a2fdaefa00
+SHA1 (patch-ab) = b252096b0bef5fee0a2f719ddc17021fd013ed64
diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa
index 2216aff94f0..f74c4f97d2b 100644
--- a/lang/coq/patches/patch-aa
+++ b/lang/coq/patches/patch-aa
@@ -1,8 +1,8 @@
-$NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
+$NetBSD: patch-aa,v 1.6 2007/12/01 13:05:37 tonio Exp $
 
---- Makefile.orig	2007-02-07 13:21:01.000000000 +0100
+--- Makefile.orig	Thu Oct 11 15:44:00 2007
 +++ Makefile
-@@ -697,22 +697,22 @@ install-coqide:: install-ide-$(HASCOQIDE
+@@ -690,22 +690,22 @@ install-coqide:: install-ide-$(HASCOQIDE
  install-ide-no:
  
  install-ide-byte: 
@@ -33,7 +33,7 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
  
  ###########################################################################
  # Pcoq: special binaries for debugging (coq-interface, parser)
-@@ -782,18 +782,18 @@ clean::
+@@ -775,18 +775,18 @@ clean::
  install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
  
  install-pcoq-binaries::
@@ -58,7 +58,7 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
  
  ###########################################################################
  # tests
-@@ -1248,21 +1248,21 @@ install-coqlight: install-binaries insta
+@@ -1244,22 +1244,21 @@ install-coqlight: install-binaries insta
  install-binaries:: install-$(BEST) install-tools
  
  install-byte::
@@ -79,6 +79,7 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
 -	$(MKDIR) $(FULLBINDIR)
  	# recopie des fichiers de style pour coqide
 -	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+-	touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
 -	cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 -	cp $(TOOLS) $(FULLBINDIR)
 +	${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR)
@@ -88,7 +89,7 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
  
  LIBFILES=$(THEORIESVO) $(CONTRIBVO)
  LIBFILESLIGHT=$(THEORIESLIGHTVO)
-@@ -1275,52 +1275,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma 
+@@ -1272,52 +1271,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma 
  OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
  
  install-library:
@@ -165,3 +166,12 @@ $NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
  #	-$(UPDATETEX)
  
  ###########################################################################
+@@ -1758,7 +1760,7 @@ depend: dependp4 ml4filesml $(BEFOREDEPE
+ 	for f in $(ML4FILES); do \
+ 	  bn=`dirname $$f`/`basename $$f .ml4`; \
+ 	  deps=`$(CAMLP4DEPS) $$f`; \
+-	  if [[ $${deps} != "" ]]; then \
++	  if [ "$${deps}" != "" ]; then \
+ 	    /bin/mv -f .depend .depend.tmp; \
+ 	    sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \
+ 	        -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \
diff --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab
new file mode 100644
index 00000000000..60630877b49
--- /dev/null
+++ b/lang/coq/patches/patch-ab
@@ -0,0 +1,13 @@
+$NetBSD: patch-ab,v 1.1 2007/12/01 13:05:37 tonio Exp $
+
+--- configure.orig	Thu Oct 11 15:13:51 2007
++++ configure
+@@ -326,7 +326,7 @@ esac
+ 
+ # this fixes a camlp4 bug under FreeBSD
+ # ("native-code program cannot do a dynamic load")
+-if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
++#if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
+ 
+ CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+