diff options
| author | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-19 10:29:01 +0200 |
| commit | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (patch) | |
| tree | 8c5648169e305e9b4038b6f04efb5a155e2f2115 /dev | |
| parent | eeab61130a2867cd7f40f86a25911b27d1962d3a (diff) | |
| parent | fa4c0aab3eace78fe283f4630e4db5ed076d267e (diff) | |
Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/critical-bugs | 10 |
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 |