From aa6d64c7de5d75f1a2625a3ec99c3efc699c5440 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Nov 2020 13:20:15 +0100
Subject: Add documentation about the soundness bug.

---
 dev/doc/critical-bugs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 066facd5db..37619833ac 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -312,6 +312,18 @@ Conversion machines
   risk: none without using -allow-sprop (off by default in 8.10.0),
         otherwise could be exploited by mistake
 
+Side-effects
+
+  component: side-effects
+  summary: polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined
+  introduced: ?
+  impacted released versions: at least from 8.6 to 8.12.0
+  impacted coqchk versions: none (no side-effects in the checker)
+  found by: ppedrot
+  exploit: test-suite/bugs/closed/bug_13330.v
+  GH issue number: #13330
+  risk: unlikely to be exploited by mistake, requires the use of unsafe tactics
+
 Conflicts with axioms in library
 
   component: library of real numbers
-- 
cgit v1.2.3