From 3d1cf0c22b1c6a8c47907296263c17abec67723e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Jan 2021 14:45:10 +0100
Subject: [PATCH] add changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7a79c72b..d0f2c9485 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   and either affine or absorbing.
 * Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
   duplicate of `fupd_plain_laterN`.
+* Strengthen `big_sepL2_app_inv` by weakening a premise (it is sufficient for
+  one of the two pairs of lists to have equal length).
 
 **Changes in `proofmode`:**
 
-- 
GitLab