summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-12-29 10:57:43 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-12-29 10:57:43 +0100
commitbf12eb93f3f6a6a824a10878878fadd59745aae0 (patch)
tree279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /CHANGES
parente0d682ec25282a348d35c5b169abafec48555690 (diff)
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES32
1 files changed, 32 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 1c094584..fa0cca0c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,35 @@
+Changes from V8.4 to V8.4pl1
+============================
+
+Bug fixes
+
+- Solved bugs :
+ #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921
+ #2930 #2941 #2878
+- Partially fixed bug : #2904
+- Various fixes concerning coq_makefile
+
+Optimizations
+
+- "Union by rank" optimization for universes contributed by J.H. Jourdan
+ and G. Sherrer (see union-find-and-coq-universes on gagallium blog).
+
+Libraries
+
+- Internal organisation of some modular libraries have slightly changed
+ due to bug #2904 (GenericMinMax, OrdersTac)
+- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml
+ (cf bug #2878).
+
+Coqide
+
+- Improved shutdown of coqtop processes spawned by coqide
+ (in particular added a missing close_on_exec primitive before forking).
+- On windows, launching coqide with the -debug option now produces
+ a log file in the user's temporary directory. The location of this
+ log file is displayed in the "About" message.
+
+
Changes from V8.4beta2 to V8.4
==============================