From b12759c2c5ba3b44f9bd34fadbf1d477fb864333 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 7 Apr 2019 22:59:56 +0200
Subject: [PATCH] Mentioned big_sepL2/sepM2 in the changelog.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 46ae8e6d0..6815004e8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -100,6 +100,10 @@ Changes in Coq:
   steps that would require unlocking subterms. Every impure wp_ tactic executes
   this tactic before doing anything else.
 * Add `big_sepM_insert_acc`.
+* Add big separating conjunctions that operate on pairs of lists (`big_sepL2`)
+  and on pairs of maps (`big_sepM2`). In the former case the lists are required
+  to have the same length, and in the latter case the maps are required to
+  have the same domains.
 * The `_strong` lemmas (e.g. `own_alloc_strong`) work for all infinite
   sets, instead of just for cofinite sets. The versions with cofinite
   sets have been renamed to use the `_cofinite` suffix.
-- 
GitLab