diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-28 16:03:16 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-28 16:06:20 +0200 |
| commit | 154229c1f21c33eae111270e490581a863181954 (patch) | |
| tree | adedba46378a15ab83b30c0bda9b4b71ed9b8830 /CHANGES | |
| parent | 551adf5a0df216bd339ee9af34d2d458fa482a72 (diff) | |
CHANGES for 8.8.1.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 11 |
1 files changed, 11 insertions, 0 deletions
@@ -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 =============================== |