Commit 7dec6f7c authored by Ralf Jung's avatar Ralf Jung

CHANGELOG: comparison change

parent 72595700
......@@ -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:
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment