Updated package to latest version, 8.5pl1. Also fixed a packaging bug

that had buildlink paths show up in the Coq_config module, and added a
patch from upstream to allow compilation with 4.03.

Changes:
Critical bugfix
- The subterm relation for the guard condition was incorrectly defined on
  primitive projections (#4588)

Plugin development tools
- add a .merlin target to the makefile

Various performance improvements (time, space used by .vo files)

Other bugfixes

- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
- Added compatibility coercions from Specif.v which were present in Coq 8.4.
- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
- Allow to unset the refinement mode of Instance in ML
- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
- Add -compat 8.4 econstructor tactics, and tests
- Add compatibility Nonrecursive Elimination Schemes
- Fixing the "No applicable tactic" non informative error message regression on apply.
- Univs: fix get_current_context (bug #4603, part I)
- Fix a bug in Program coercion code
- Fix handling of arity of definitional classes.
- #4630: Some tactics are 20x slower in 8.5 than 8.4.
- #4627: records with no declared arity can be template polymorphic.
- #4623: set tactic too weak with universes (regression)
- Fix incorrect behavior of CS resolution
- #4591: Uncaught exception in directory browsing.
- CoqIDE is more resilient to initialization errors.
- #4614: "Fully check the document" is uninterruptable.
- Try eta-expansion of records only on non-recursive ones
- Fix bug when a sort is ascribed to a Record
- Primitive projections: protect kernel from erroneous definitions.
- Fixed bug #4533 with previous Keyed Unification commit
- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
- Fix strategy of Keyed Unification
- #4608: Anomaly "output_value: abstract value (outside heap)".
- #4607: do not read native code files if native compiler was disabled.
- #4105: poor escaping in the protocol between CoqIDE and coqtop.
- #4596: [rewrite] broke in the past few weeks.
- #4533 (partial): respect declared global transparency of projections in unification.ml
- #4544: Backtrack on using full betaiota reduction during keyed unification.
- #4540: CoqIDE bottom progress bar does not update.
- Fix regression from 8.4 in reflexivity
- #4580: [Set Refine Instance Mode] also used for Program Instance.
- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
- STM: Print/Extraction have to be skipped if -quick
- #4542: CoqIDE: STOP button also stops workers
- STM: classify some variants of Instance as regular `Fork nodes.
- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
- Do not give a name to anonymous evars anymore. See bug #4547.
- STM: always stock in vio files the first node (state) of a proof
- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
- Don't fail fatally if PATH is not set.
- #4537: Coq 8.5 is slower in typeclass resolution.
- #4522: Incorrect "Warning..." on windows.
- #4373: coqdep does not know about .vio files.
- #3826: "Incompatible module types" is uninformative.
- #4495: Failed assertion in metasyntax.ml.
- #4511: evar tactic can create non-typed evars.
- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
- #4519: oops, global shadowed local universe level bindings.
- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
- #4548: Coqide crashes when going back one command

1 files changed, 6 insertions, 6 deletions

diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 15da4310035..b2e9ac07091 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,9 +1,9 @@
-$NetBSD: distinfo,v 1.24 2016/02/06 16:08:36 jaapb Exp $
+$NetBSD: distinfo,v 1.25 2016/07/02 10:17:18 jaapb Exp $
 
-SHA1 (coq-8.5.tar.gz) = 0a0d124b1869d7e20cfcf3f71f086488c146f883
-RMD160 (coq-8.5.tar.gz) = 551d35ac96436d98112fa1a17bcc075ee307c627
-SHA512 (coq-8.5.tar.gz) = 28835a9dc4c926f97b14d23fe746e45e17942003e29807ec59f301eb0b697d704f05afc4cccd31b83bc27e9877d079d00e94a2101ba16ae32f4134e90ad011fb
-Size (coq-8.5.tar.gz) = 5346653 bytes
+SHA1 (coq-8.5pl1.tar.gz) = 92722ffc2be6948e0074b211bb556ad4b911ebd6
+RMD160 (coq-8.5pl1.tar.gz) = 04c540ab1033fd6b0e4c121b73ed56557708e7a5
+SHA512 (coq-8.5pl1.tar.gz) = c9a5bba1abc3b2216cb43595230387751277412988b44af1555ffccdc109a9eef69422867e0062d92dfc73ffcbbe24f53ff583224c28cae3f9bda1ae21dd547b
+Size (coq-8.5pl1.tar.gz) = 5366774 bytes
 SHA1 (patch-Makefile.build) = 1b711ef9490a07c9d02b5a8ca9a38c252e322b4f
-SHA1 (patch-Makefile.common) = 67131e197d25a087d845dfa6fa93729f0b2eaa00
+SHA1 (patch-Makefile.common) = f53dd334d3e14a0e0c3ef91bac9a6c1745cbb591
 SHA1 (patch-configure.ml) = 6e2f44091216348a12131592bf29f0f7fd93a4fe