From 1e029b180a0953c4c8f14965f549141f93c492c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Oct 2020 10:30:29 +0100
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 719bd4274..16a52ec96 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -119,6 +119,10 @@ With this release, we dropped support for Coq 8.9.
   `big_sepL_dup`, `big_sepM_dup`, `big_sepS_dup`. Instead of having `□ (P -∗ P ∗
   P)` as an assumption these lemmas now assume `P` to be an instance of
   `Duplicable`.
+* Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used
+  and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
+* Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used
+  by `gen_heap`.
 
 **Changes in `program_logic`:**
 
-- 
GitLab