diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 10 |
2 files changed, 16 insertions, 0 deletions
@@ -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 |