From b42f8f52583d562aef972eb7da003be92ccc3d9a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Nov 2020 13:28:28 +0100
Subject: [PATCH] extend changelog

---
 CHANGELOG.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2fdd7bb0b..719bd4274 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -111,8 +111,11 @@ With this release, we dropped support for Coq 8.9.
   an authoritative, monotonically-increasing `nat` with a proposition giving a
   persistent lower bound. See `base_logic.lib.mnat` for further details.
 * Add a class, `Duplicable`, for duplicable propositions. The lemmas
-  `intuitionistically_sep_dup` and `plainly_sep_duplicable` are now instances. A
-  few lemmas are changed to use the new class: `inv_combine_dup_l`,
+  `intuitionistically_sep_dup`, `persistently_sep_dup`,
+  `plainly_sep_duplicable`, and `persistent_sep_dup` are now instances. This
+  means they are now uni-directional; use `duplicable_equiv` to obtain the
+  bidirectional version.
+  A few lemmas are changed to use the new class: `inv_combine_dup_l`,
   `big_sepL_dup`, `big_sepM_dup`, `big_sepS_dup`. Instead of having `□ (P -∗ P ∗
   P)` as an assumption these lemmas now assume `P` to be an instance of
   `Duplicable`.
-- 
GitLab