aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-03-26 23:00:05 +0100
committerGaëtan Gilbert2019-03-26 23:00:05 +0100
commit2c37c0e7eea9b8406e534e93881158bb6919ed38 (patch)
tree0dac1382c8d44eecb31e3390beb5b1ece1704263 /dev
parente8fd832d9e487fa57e2efe627223d04ff2977fa9 (diff)
Incorrect details in critical bug info (prop_set_proof_irrelevance)
Diffstat (limited to 'dev')
-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 8d78559c0d..dc7789df89 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -63,8 +63,8 @@ Typing constructions
impacted coqchk versions: ?
fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
found by: Georgi Guninski
- exploit: test-suite/bugs/closed/4294.v
- GH issue number: #4294
+ exploit: test-suite/failure/prop_set_proof_irrelevance.v
+ GH issue number: none?
risk: ?
Module system