Update of package to version 8.4pl4. Changes include:

Changes from V8.4pl3 to V8.4pl4
===============================

WARNING:
The current logic of Coq is now known to be inconsistent with
  Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.
For more details, see:
  https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD
or
  https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD

Kernel

- Unsound check of elimination sort.
- Fix guard condition for nested cofixpoints.
- Univ constraints of module subtyping were not propagated.

Tactics

- A new option "Set Stable Omega" ensures that repeated identical calls
  to omega will produce identical proof terms. This option is off by default
  for maximal compatibility, but should be pretty safe to activate.
- The interpretation of the open_constr tactic argument was erroneously
  firing type classes resolution in some corner cases.  This has been
  fixed.  The tactic argument type open_constr_wTC is provided for retro
  compatibility purposes.
- Fixing bug (fixing precedence of ltac variables over variables in
  env) introduces rare and justified tactic failure.

Bug fixes

- micromega: solved an ambiguous symbol resolution.
- Coq always uses / as separator between directories on all platforms.
- remove trailing '\r' from file names returned by coqtop.
- bug correction in proving inversion principles for Function.
- ocamlbuild: minor fixes related to camlp4 and cross-compilation.

Changes from V8.4pl2 to V8.4pl3
===============================

Ide_slave XML interface

- 20120712, 20130419 : Invalidated protocol versions
- From 20130419 extra datastructure : union
   (Inl "" = <union val="in_l"><string></string></union>,
    Inr _ = <union val="in_r">...)
- 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not
  handle by coqide v8.4. A message has a level and a content (of string).
  Message levels are Debug of string, Info, Notice, Warning and Error.
- 20130425 :
  * new toplevel entry : feedback, once again not send by coqtop v8.4 and not
  handle by coqide v8.4. A feedback gives the id of the sentence it provides info
  about and a content. Feedback contents are Processed, AddedAxiom and
  GlobRef of Util.loc * string * string * string * string
  * <call val="interp"> must provide an attribute id of type int. It is OK in
  coqtop v8.4 to alwais send <call val="interp" id="0">

Bug fixes

- Fixing a significant efficiency leak in the code of the field tactic.
- Fix caching of local hint database in typeclasses eauto which could
  miss some hypotheses.
- Fix automatic solving of obligation in program, which was not trying
  to solve obligations that had no undefined dependencies left.

3 files changed, 6 insertions, 32 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 81527d9638a..3bb8ad8691a 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.74 2014/05/05 00:48:05 ryoon Exp $
+# $NetBSD: Makefile,v 1.75 2014/05/13 14:52:28 jaapb Exp $
 #
 
-DISTNAME=	coq-8.4pl2
-PKGREVISION=	14
+DISTNAME=	coq-8.4pl4
 CATEGORIES=	lang math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 3cd926d82e2..fae00471b6a 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,7 +1,6 @@
-$NetBSD: distinfo,v 1.18 2013/10/27 22:22:31 joerg Exp $
+$NetBSD: distinfo,v 1.19 2014/05/13 14:52:28 jaapb Exp $
 
-SHA1 (coq-8.4pl2.tar.gz) = adcef430b8e27663e8ea075e646112f7d4d51fa6
-RMD160 (coq-8.4pl2.tar.gz) = 4860eaff4c8f0a235d3fcf162199eaa5fe1db2da
-Size (coq-8.4pl2.tar.gz) = 4145112 bytes
+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-configure) = 1ad232e16d397a762e61c000d1859c70d2447fc1
diff --git a/lang/coq/patches/patch-configure b/lang/coq/patches/patch-configure
deleted file mode 100644
index d5874e20ae7..00000000000
--- a/lang/coq/patches/patch-configure
+++ /dev/null
@@ -1,24 +0,0 @@
-$NetBSD: patch-configure,v 1.2 2013/10/27 22:22:31 joerg Exp $
-
-Accept GNU Make 4 and later.
-
---- configure.orig	2013-10-17 13:00:47.000000000 +0000
-+++ configure
-@@ -111,7 +111,7 @@ coq_debug_flag_opt=
- coq_profile_flag=
- coq_annotate_flag=
- best_compiler=opt
--cflags="-fno-defer-pop -Wall -Wno-unused"
-+cflags="-Wall -Wno-unused"
- natdynlink=yes
- 
- local=false
-@@ -335,7 +335,7 @@ if [ "$MAKE" != "" ]; then
-   MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
-   MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
-   MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
--  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-+  if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-       echo "You have GNU Make $MAKEVERSION. Good!"
-   else
-       OK="no"