Merge tag 'upstream/8.4pl3dfsg'

Upstream version 8.4pl3dfsg

1 files changed, 31 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index a696ad71..5df109a1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,34 @@
+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
+
+- Solved bugs:
+  #2230 #2837 #2846 #2987 #3003 #3001 #3013 #3023 #3025 #3036 #3118 #3169
+  #(3150, 3151, 3152, 3153)
+- 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.
+
 Changes from V8.4pl1 to V8.4pl2
 ===============================