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

---
 dev/doc/critical-bugs | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dev')

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