Commit 180cd032 authored by Ralf Jung's avatar Ralf Jung

revert accidentally changed changelog

parent 292a1a38
......@@ -115,7 +115,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
* Slightly weaker notion of atomicity: an expression is atomic if it reduces in
one step to something that does not reduce further.
* Changed notation for embedding Coq assertions into Iris. The new notation is
⌜φ⌝. Also removed `=` and `##` from the Iris scope. (The old notations are
⌜φ⌝. Also removed `=` and `` from the Iris scope. (The old notations are
provided in `base_logic.deprecated`.)
* Up-closure of namespaces is now a notation (↑) instead of a coercion.
* With invariants and the physical state being handled in the logic, there is no
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment