aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/critical-bugs
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/critical-bugs')
-rw-r--r--dev/doc/critical-bugs10
1 files changed, 10 insertions, 0 deletions
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