aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-11-08 11:20:40 +0100
committerThéo Zimmermann2019-11-08 11:20:40 +0100
commitae7d7e162f3febcad5dd8678f3369cbecccf8f43 (patch)
tree05bfcf1b3518a470f11d275480740abc88467bc1
parent64ddd9ac0c34e560a0640297e2e23b6aaf074810 (diff)
parent7233d98a79894c6be1cbe99d003982b0f6a5c37b (diff)
Merge PR #11042: The "univ poly can capture global univs" checker side bug is fixed
Reviewed-by: Zimmi48
-rw-r--r--dev/doc/critical-bugs4
1 files changed, 2 insertions, 2 deletions
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