From 68ec156bde9e050f92b3d11d56d2f30d8468da95 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Nov 2020 11:59:49 +0100
Subject: [PATCH] CHANGELOG.
---
CHANGELOG.md | 1 +
1 file changed, 1 insertion(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 897889c3b..231866b29 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,6 +58,7 @@ 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.
**Changes in `proofmode`:**
--
GitLab