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.
edc9ce12d3