From 6cafb5364b463e88dc109b3ab6aec22d025cf897 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2021 11:36:14 +0100
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fe61684a7..18a5bf2d2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -102,6 +102,20 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Add lemmas for big-ops of magic wands: `big_sepL_wand`, `big_sepL2_wand`,
   `big_sepM_wand`, `big_sepM2_wand`, `big_sepS_wand`, `big_sepMS_wand`.
 
+* Add `fupd_mask_intro` which can be conveniently `iApply`ed to goals of the
+  form `|={E1,E2}=>` to get rid of the `fupd` in the goal if `E2 ⊆ E1`. The
+  lemma `fupd_mask_weaken Enew` can be `iApply`ed to shrink the first mask to
+  `Enew` without getting rid of the modality; the same effect can also be
+  obtained slightly more conveniently by using `iMod` with `fupd_mask_subseteq
+  Enew`. To make the new names work, rename some existing lemmas:
+  `fupd_intro_mask` → `fupd_mask_intro_subseteq`,
+  `fupd_intro_mask'` → `fupd_mask_subseteq` (implicit arguments also changed
+  here), `fupd_mask_weaken` → `fupd_mask_intro_discard`. Remove `fupd_mask_same`
+  since it was unused and obscure.  In the `BiFUpd` axiomatization, rename
+  `bi_fupd_mixin_fupd_intro_mask` to `bi_fupd_mixin_fupd_mask_subseteq` and
+  weaken the lemma to be specifically about `emp` (the stronger version can be
+  derived).
+
 **Changes in `proofmode`:**
 
 * The proofmode now preserves user-supplied names for existentials when using
-- 
GitLab