Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)

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
 ===========================