Add entry for universe polymorphism critical bug

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index bca4788058..9975cb9ecd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -205,6 +205,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
 ===========================