Updated lang/coq to the newest version, 8.4pl1. Changes include:

Bug fixes

- Solved bugs :
  #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921
  #2930 #2941 #2878
- Partially fixed bug : #2904
- Various fixes concerning coq_makefile

Optimizations

- "Union by rank" optimization for universes contributed by J.H. Jourdan
  and G. Sherrer (see union-find-and-coq-universes on gagallium blog).

Libraries

- Internal organisation of some modular libraries have slightly changed
  due to bug #2904 (GenericMinMax, OrdersTac)
- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml
  (cf bug #2878).

Coqide

- Improved shutdown of coqtop processes spawned by coqide
  (in particular added a missing close_on_exec primitive before forking).
- On windows, launching coqide with the -debug option now produces
  a log file in the user's temporary directory. The location of this
  log file is displayed in the "About" message.

4 files changed, 7 insertions, 55 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index fb8fb64b466..a1c826d3b47 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,10 +1,9 @@
-# $NetBSD: Makefile,v 1.53 2012/12/15 10:36:28 ryoon Exp $
+# $NetBSD: Makefile,v 1.54 2013/01/22 15:32:03 jaapb Exp $
 #
 
-DISTNAME=	coq-8.4
-PKGREVISION=	2
+DISTNAME=	coq-8.4pl1
 CATEGORIES=	lang math
-MASTER_SITES=	http://coq.inria.fr/distrib/V8.4/files/
+MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION}/files/
 
 MAINTAINER=	jaapb@NetBSD.org
 HOMEPAGE=	http://coq.inria.fr/
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index b528bb8eff2..364220336c5 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,8 +1,6 @@
-$NetBSD: distinfo,v 1.14 2012/10/29 11:33:17 jaapb Exp $
+$NetBSD: distinfo,v 1.15 2013/01/22 15:32:03 jaapb Exp $
 
-SHA1 (coq-8.4.tar.gz) = 2987aa418dd96a0df7284afe296293cb28814ef5
-RMD160 (coq-8.4.tar.gz) = 6824f9542c823c7d943a59acefb90ff9c9dbe37a
-Size (coq-8.4.tar.gz) = 4134779 bytes
+SHA1 (coq-8.4pl1.tar.gz) = 23d403dbe9e410a99c584d0210dc527950051679
+RMD160 (coq-8.4pl1.tar.gz) = fa472852de474ed5b83ddd4bd5a303f32b5dba94
+Size (coq-8.4pl1.tar.gz) = 4139808 bytes
 SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4
-SHA1 (patch-ide_preferences.ml) = 625b8e7fe7b4f1612c7f43bd634070aff928fdfb
-SHA1 (patch-ide_utils_okey.ml) = d61ad0e2ea23c531bb4f5e9540f8581a72b54da8
diff --git a/lang/coq/patches/patch-ide_preferences.ml b/lang/coq/patches/patch-ide_preferences.ml
deleted file mode 100644
index 0c11c0ce910..00000000000
--- a/lang/coq/patches/patch-ide_preferences.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-$NetBSD: patch-ide_preferences.ml,v 1.1 2012/10/29 11:33:18 jaapb Exp $
-
-Correct for compilation with lablgtk 2.16
---- ide/preferences.ml.orig	2012-08-08 18:54:37.000000000 +0000
-+++ ide/preferences.ml
-@@ -35,6 +35,10 @@ let mod_to_str (m:Gdk.Tags.modifier) =
-     | `MOD5 -> "<Mod5>"
-     | `CONTROL -> "<Control>"
-     | `SHIFT -> "<Shift>"
-+    | `HYPER -> "<Hyper>"
-+    | `META -> "<Meta>"
-+    | `RELEASE -> ""
-+    | `SUPER -> "<Super>"
-     |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
- 
- let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
diff --git a/lang/coq/patches/patch-ide_utils_okey.ml b/lang/coq/patches/patch-ide_utils_okey.ml
deleted file mode 100644
index 8ed5cfd5ef5..00000000000
--- a/lang/coq/patches/patch-ide_utils_okey.ml
+++ /dev/null
@@ -1,29 +0,0 @@
-$NetBSD: patch-ide_utils_okey.ml,v 1.1 2012/10/29 11:33:18 jaapb Exp $
-
-Correct for compilation with lablgtk 2.16
---- ide/utils/okey.ml.orig	2006-03-08 11:44:47.000000000 +0000
-+++ ide/utils/okey.ml
-@@ -47,6 +47,10 @@ let int_of_modifier = function
-   | `BUTTON3 -> 1024
-   | `BUTTON4 -> 2048
-   | `BUTTON5 -> 4096
-+  | `HYPER -> 1 lsl 22
-+  | `META -> 1 lsl 20
-+  | `RELEASE -> 1 lsl 30
-+  | `SUPER -> 1 lsl 21
- 
- let print_modifier l =
-   List.iter
-@@ -65,7 +69,11 @@ let print_modifier l =
- 	  | `BUTTON2 -> "B2"
- 	  | `BUTTON3 -> "B3"
- 	  | `BUTTON4 -> "B4"
--	  | `BUTTON5 -> "B5")
-+	  | `BUTTON5 -> "B5"
-+	  | `HYPER -> "HYPER"
-+	  | `META -> "META"
-+	  | `RELEASE -> ""
-+	  | `SUPER -> "SUPER")
- 	    m)^" ")
-     )
-     l;