From c9e330943a2bd1aa709139f0ea36fb17c6f6afa7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 May 2021 15:23:52 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 768bf1001..2aaa768eb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,12 @@ Coq 8.11 is no longer supported in this version of Iris.
   is not very well-behaved.
 * Extend `gmap_view` with lemmas for "big" operations on maps.
 
+**Changes in `bi`:**
+
+* Add new lemmas `big_sepM2_delete_l` and `big_sepM2_delete_r`.
+* Rename `big_sepM2_lookup_1` → `big_sepM2_lookup_l` and
+  `big_sepM2_lookup_2` → `big_sepM2_lookup_r`.
+
 **Changes in `proofmode`:**
 
 * Add support for pure names `%H` in intro patterns. This is now natively
@@ -77,6 +83,8 @@ s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_va
 s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
+s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
+s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 EOF
 ```
 
-- 
GitLab