From fe2a377efbb5b96561df2d924ac15ed059fbf117 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Nov 2020 12:14:29 +0100
Subject: [PATCH] extend changelog explanation

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 231866b29..c8b9617a3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,7 +58,8 @@ With this release, we dropped support for Coq 8.9.
 
 * Add big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall` and
   `big_sepL2_forall`, `big_sepMS_forall`, `big_sepMS_impl`, and `big_sepMS_dup`.
-* Remove `bi.tactics` with tactics that predate the proofmode.
+* Remove `bi.tactics` with tactics that predate the proofmode (and that have not
+  been working properly for quite some time).
 
 **Changes in `proofmode`:**
 
-- 
GitLab