From 7aa4ad8b61a1917ddc0596525945c4650d18fb86 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 2 Jul 2020 12:22:20 +0200
Subject: [PATCH] Mention change to lemmas in changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index caee82ff7..dd1775bc2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -211,6 +211,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   As part of this, the lemmas about the 3-mask variant were changed to be about
   the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more
   consistent argument order for its masks.
+* Slightly strengthen the lemmas `big_sepL_nil'`, `big_sepL2_nil'`,
+  `big_sepM_nil'` `big_sepM2_empty'`, `big_sepS_empty'`, and `big_sepMS_empty'`.
+  They now only require that the argument `P` is affine instead of the whole BI
+  being affine.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
-- 
GitLab