From f455b5d4f6c2b39a6c718811d0508286aea940b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Jul 2019 10:57:09 +0200
Subject: [PATCH] changelog for comparison changes

---
 CHANGELOG.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b3f380d64..1b6f567af 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,7 +43,11 @@ Changes in heap_lang:
   typically provided in systems languages (C, C++, Rust).
   The comparison by this operation also got weakened to be efficiently
   implementable: CmpXchg may only be used to compare "unboxed" values that can
-  be represented in a single machine word.
+  be represented in a single machine word. It is sufficient if one of the two
+  compared values is unboxed.
+* For consistency, the restrictions CmpXchg imposes on comparison also apply to
+  the `=` binary operator. This also fixes the long-standing problem that that
+  operator allowed compared closures with each other.
 * Implement prophecy variables using the new support for "observations".
 * heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.
@@ -56,10 +60,6 @@ Changes in heap_lang:
 * heap_lang now has support for allocating, accessing and reasoning about arrays
   (continuously allocated regions of memory).
 * One can now assign "meta" data to heap_lang locations.
-* For comparison operation (the binary operator and CmpXchg), all closures are
-  "normalized" to the same.  This makes all closures indistinguishable from each
-  other while remaining unqueal to anything else.  We also use the same
-  "normalization" to make sure all prophecy variables seem equal to `()`.
 
 Changes in Coq:
 
-- 
GitLab