CHANGELOG.

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
 ```