From 7233d98a79894c6be1cbe99d003982b0f6a5c37b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 4 Nov 2019 16:28:09 +0100
Subject: The "univ poly can capture global univs" checker side bug is fixed

(by the checker refactor AFAICT)

+ fix commit for the coqtop side fix (it got rebased at some point)

Close #10705
---
 dev/doc/critical-bugs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 6d90ced12d..0631b3ad59 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -112,8 +112,8 @@ Universes
   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
+  impacted coqchk versions: V8.5 to V8.9
+  fixed in: ec4aa4971f (58e1d0f200 for the checker)
   found by: Gaëtan Gilbert
   exploit: test-suite/misc/poly-capture-global-univs
   GH issue number: #8341
-- 
cgit v1.2.3