From c2f90237949d777b5ce3670bd26ac2814ad0e71c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Nov 2020 13:51:02 +0100
Subject: [PATCH] more informative changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4612e8212..a7e0ac0c0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,8 +123,8 @@ With this release, we dropped support for Coq 8.9.
   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`.
-* Strengthen `mapsto_valid_2` to provide both a bound on the fractions and
-  agreement.
+* Strengthen `mapsto_valid_2` conclusion from `✓ (q1 + q2)%Qp` to
+  `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
 
 **Changes in `program_logic`:**
 
-- 
GitLab