aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-28 16:03:16 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-28 16:06:20 +0200
commit154229c1f21c33eae111270e490581a863181954 (patch)
treeadedba46378a15ab83b30c0bda9b4b71ed9b8830
parent551adf5a0df216bd339ee9af34d2d458fa482a72 (diff)
CHANGES for 8.8.1.
-rw-r--r--CHANGES11
1 files changed, 11 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 44186d30c..75f4df06a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,7 @@ Changes from 8.8.0 to 8.8.1
Kernel
- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with modules and algebraic universes (#7695)
- Fix a critical bug with inlining of polymorphic constants (#7615).
- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was
present since 8.5.
@@ -100,6 +101,16 @@ Notations
- Fixed unexpected collision between only-parsing and only-printing
notations (issue #7462).
+Windows installer
+
+- The Windows installer now includes external packages Ltac2 and Equations
+ (it included the Bignums package since 8.8+beta1).
+
+Many other bug fixes, documentation improvements (including fixes of
+regressions due to the Sphinx migration), and user message improvements
+(for details, see the 8.8.1 milestone at
+https://github.com/coq/coq/milestone/13?closed=1).
+
Changes from 8.8+beta1 to 8.8.0
===============================