From fa4c0aab3eace78fe283f4630e4db5ed076d267e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 30 Aug 2018 13:17:52 +0200
Subject: Add entry for universe polymorphism critical bug

---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'CHANGES')

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
 ===========================
 
-- 
cgit v1.2.3