From 7dec6f7c5c8da3615bddbbd37a53306ea915f27d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 19 Jun 2019 08:24:07 +0200 Subject: [PATCH] CHANGELOG: comparison change --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 66abeb752..6e222c2a0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -50,6 +50,10 @@ 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 CAS), 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