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.

---
 doc/sphinx/changes.rst | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 8da5014125..f1bcd2fb44 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1224,6 +1224,13 @@ Changes in 8.12.1
   <https://github.com/coq/coq/pull/12738>`_, fixes `#7015
   <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert).
 
+- **Fixed:**
+  Polymorphic side-effects inside monomorphic definitions were incorrectly
+  handled as not inlined. This allowed deriving an inconsistency
+  (`#13331 <https://github.com/coq/coq/pull/13331>`_,
+  fixes `#13330 <https://github.com/coq/coq/issues/13330>`_,
+  by Pierre-Marie Pédrot).
+
 **Notations**
 
 - **Fixed:**
-- 
cgit v1.2.3