CVS commit: pkgsrc/lang/coq

["Jaap Boender" <jaapb%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   jaapb
Date:           Tue May 13 14:52:28 UTC 2014

Modified Files:
        pkgsrc/lang/coq: Makefile distinfo
Removed Files:
        pkgsrc/lang/coq/patches: patch-configure

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.


To generate a diff of this commit:
cvs rdiff -u -r1.74 -r1.75 pkgsrc/lang/coq/Makefile
cvs rdiff -u -r1.18 -r1.19 pkgsrc/lang/coq/distinfo
cvs rdiff -u -r1.2 -r0 pkgsrc/lang/coq/patches/patch-configure

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.