diff --git a/CHANGELOG.md b/CHANGELOG.md index 897889c3b519e074238f786bc7e162a37dfd33e8..231866b29b1138f4e59c4db8225d3e812735eb03 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`:**