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 ++++++
 dev/doc/critical-bugs | 10 ++++++++++
 2 files changed, 16 insertions(+)

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
 ===========================
 
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 6166d24b70..8d78559c0d 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -109,6 +109,16 @@ Universes
   GH issue number: none
   risk: unlikely to be activated by chance
 
+  component: universe polymorphism
+  summary: universe polymorphism can capture global universes
+  impacted released versions: V8.5 to V8.8
+  impacted coqchk versions: V8.5 to current (NOT FIXED)
+  fixed in: 2385b5c1ef
+  found by: Gaëtan Gilbert
+  exploit: test-suite/misc/poly-capture-global-univs
+  GH issue number: #8341
+  risk: unlikely to be activated by chance (requires a plugin)
+
 Primitive projections
 
   component: primitive projections, guard condition
-- 
cgit v1.2.3