I've been running this coq update for a while. ok?
Here are the changes:
Compilation
- Coq compilation made possible with forthcoming ocaml 4.03.
Bug fixes
- Bug #4157: proof of False via vm compute on inductive with many
constructors.
- Bug #3491: anomaly when building _rect scheme in the presence of let-ins
and recursively non-uniform parameters.
- Bug #2447: stack Overflow in congruence.
- Bug #3892: ensure that notation variables do not capture names hidden
behind another notation.
- Bug #3843: cmxs installation on cygwin.
- Bug #3837: Function graph interacts poorly with existential types.
- Bug #3824: Eval vm_compute fails whereas Eval compute succeeds.
- Bug #3723 and #3787: reinitialization of camlp5 empty levels.
- Fix depelim tactic.
Documentation
- Bug #4127: command for locating exists notation in refman changed.
- Various improvements of the Reference Manual (especially its html
version)
Index: Makefile
===================================================================
RCS file: /home/cvs/ports/math/coq/Makefile,v
retrieving revision 1.30
diff -u -p -u -r1.30 Makefile
--- Makefile 22 Jan 2015 21:17:47 -0000 1.30
+++ Makefile 22 Apr 2015 13:10:28 -0000
@@ -2,7 +2,7 @@
COMMENT= proof assistant based on a typed lambda calculus
-V= 8.4pl5
+V= 8.4pl6
DISTNAME= coq-$V
CATEGORIES= math
Index: distinfo
===================================================================
RCS file: /home/cvs/ports/math/coq/distinfo,v
retrieving revision 1.12
diff -u -p -u -r1.12 distinfo
--- distinfo 18 Nov 2014 02:00:52 -0000 1.12
+++ distinfo 22 Apr 2015 13:10:44 -0000
@@ -1,2 +1,2 @@
-SHA256 (coq-8.4pl5.tar.gz) = NYFat4pY1yeZ6sqrFVQnYgqwcWd4gspsmNe/7JfSUkU=
-SIZE (coq-8.4pl5.tar.gz) = 4070062
+SHA256 (coq-8.4pl6.tar.gz) = pUCiMamXCkk1PKA581RGFv+GogiWarHFk3ea4TyR69Y=
+SIZE (coq-8.4pl6.tar.gz) = 4099815
Index: patches/patch-configure
===================================================================
RCS file: /home/cvs/ports/math/coq/patches/patch-configure,v
retrieving revision 1.5
diff -u -p -u -r1.5 patch-configure
--- patches/patch-configure 26 Mar 2014 03:27:26 -0000 1.5
+++ patches/patch-configure 22 Apr 2015 13:10:53 -0000
@@ -1,8 +1,8 @@
$OpenBSD: patch-configure,v 1.5 2014/03/26 03:27:26 daniel Exp $
---- configure.orig Sat Dec 21 03:03:14 2013
-+++ configure Mon Dec 30 19:04:42 2013
-@@ -897,7 +897,7 @@ case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM
+--- configure.orig Thu Apr 9 09:59:35 2015
++++ configure Wed Apr 22 09:10:47 2015
+@@ -900,7 +900,7 @@ case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM
*/true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath
'$COQTOP'/kernel/byterun";;
*)
COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /home/cvs/ports/math/coq/pkg/PFRAG.dynlink-native,v
retrieving revision 1.2
diff -u -p -u -r1.2 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 26 Mar 2014 03:27:26 -0000 1.2
+++ pkg/PFRAG.dynlink-native 22 Apr 2015 13:42:00 -0000
@@ -19,29 +19,29 @@ lib/coq/parsing/highparsing.a
lib/coq/parsing/highparsing.cmxa
lib/coq/parsing/parsing.a
lib/coq/parsing/parsing.cmxa
-lib/coq/plugins/cc/cc_plugin.cmxs
-lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
-lib/coq/plugins/extraction/extraction_plugin.cmxs
-lib/coq/plugins/field/field_plugin.cmxs
-lib/coq/plugins/firstorder/ground_plugin.cmxs
-lib/coq/plugins/fourier/fourier_plugin.cmxs
-lib/coq/plugins/funind/recdef_plugin.cmxs
-lib/coq/plugins/micromega/micromega_plugin.cmxs
-lib/coq/plugins/nsatz/nsatz_plugin.cmxs
-lib/coq/plugins/omega/omega_plugin.cmxs
-lib/coq/plugins/quote/quote_plugin.cmxs
-lib/coq/plugins/ring/ring_plugin.cmxs
-lib/coq/plugins/romega/romega_plugin.cmxs
-lib/coq/plugins/rtauto/rtauto_plugin.cmxs
-lib/coq/plugins/setoid_ring/newring_plugin.cmxs
-lib/coq/plugins/subtac/subtac_plugin.cmxs
-lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
-lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
-lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
-lib/coq/plugins/syntax/r_syntax_plugin.cmxs
-lib/coq/plugins/syntax/string_syntax_plugin.cmxs
-lib/coq/plugins/syntax/z_syntax_plugin.cmxs
-lib/coq/plugins/xml/xml_plugin.cmxs
+@bin lib/coq/plugins/cc/cc_plugin.cmxs
+@bin lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
+@bin lib/coq/plugins/extraction/extraction_plugin.cmxs
+@bin lib/coq/plugins/field/field_plugin.cmxs
+@bin lib/coq/plugins/firstorder/ground_plugin.cmxs
+@bin lib/coq/plugins/fourier/fourier_plugin.cmxs
+@bin lib/coq/plugins/funind/recdef_plugin.cmxs
+@bin lib/coq/plugins/micromega/micromega_plugin.cmxs
+@bin lib/coq/plugins/nsatz/nsatz_plugin.cmxs
+@bin lib/coq/plugins/omega/omega_plugin.cmxs
+@bin lib/coq/plugins/quote/quote_plugin.cmxs
+@bin lib/coq/plugins/ring/ring_plugin.cmxs
+@bin lib/coq/plugins/romega/romega_plugin.cmxs
+@bin lib/coq/plugins/rtauto/rtauto_plugin.cmxs
+@bin lib/coq/plugins/setoid_ring/newring_plugin.cmxs
+@bin lib/coq/plugins/subtac/subtac_plugin.cmxs
+@bin lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
+@bin lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
+@bin lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
+@bin lib/coq/plugins/syntax/r_syntax_plugin.cmxs
+@bin lib/coq/plugins/syntax/string_syntax_plugin.cmxs
+@bin lib/coq/plugins/syntax/z_syntax_plugin.cmxs
+@bin lib/coq/plugins/xml/xml_plugin.cmxs
lib/coq/pretyping/pretyping.a
lib/coq/pretyping/pretyping.cmxa
lib/coq/proofs/proofs.a
Index: pkg/PLIST
===================================================================
RCS file: /home/cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.7
diff -u -p -u -r1.7 PLIST
--- pkg/PLIST 26 Mar 2014 03:27:26 -0000 1.7
+++ pkg/PLIST 22 Apr 2015 13:42:00 -0000
@@ -597,6 +597,7 @@ lib/coq/theories/Logic/Epsilon.vo
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
