Log message:
Updated coq to version 8.4pl6. Changes from previous version include (apart
from bugfixes):

- Coq compilation made possible with forthcoming ocaml 4.03.
- command for locating exists notation in refman changed.
- Various improvements of the Reference Manual (especially its html version)
- implicit arguments of local definitions fixed (possible
  source of incompatibilities).
- New command "Print Debug GC".
- Function cannot define graph.
- Optimizing compilation of pattern matching.
- Better inference of impossible cases in pattern-matching.
- Evar leak in pattern-matching compilation
- ill-typed replacement in "change ... with ...".
- unbound evars in "change ... with ...".
- wrong return clause of a match pattern in Ltac.
- cleared local hints for autounfold.
- cleared local hints for autounfold.
- lost evars in "change ... with ...".
- supporting let-ins in constructors for vm_compute
- unfortunate typo in compare_height.
- unfortunate typos in absorption lemmas over bool.
- Full support of utf8 Greek letters (block U0370) in coqdoc

Log message:
Revbump after updating textproc/icu

Log message:
Revbump associated with update of lang/ocaml.

Log message:
Changed package dependencies to reflect lablgtk name change.

Log message:
Revbump because of ocaml 4.02, added compilation patch (already in
repository upstream) and updated package to use ocaml.mk framework.

Log message:
Revbump after updating libwebp and icu

Log message:
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.

Log message:
Recursive revbump from x11/pixman
Fix PR pkg/48777

Log message:
recursive bump from icu shlib major bump.

Log message:
Recursive PKGREVISION bump for OpenSSL API version bump.