Commit 6c06af44 authored by Ralf Jung's avatar Ralf Jung
Browse files


parent 00444b07
Pipeline #3231 passed with stage
in 10 minutes and 54 seconds
......@@ -21,6 +21,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Renaming and moving things around: uPred and the rest of the base logic are
in `base_logic`, while `program_logic` is for everything involving the
general Iris notion of a language.
* [#] 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 provided in `base_logic.deprecated`.)
Supports Markdown
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