aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES6
1 files changed, 6 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 46266a1bd0..1bf0e0edd4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -221,6 +221,12 @@ Tools
and `print-pretty-single-time-diff` now correctly label the "before" and
"after" columns, rather than swapping them.
+Kernel
+
+- The kernel does not tolerate capture of global universes by
+ polymorphic universe binders, fixing a soundness break (triggered
+ only through custom plugins)
+
Changes from 8.8.0 to 8.8.1
===========================