Commit 598a6902 authored by Ralf Jung's avatar Ralf Jung

wp_fork changelog

parent d7934087
...@@ -24,8 +24,8 @@ Changes in and extensions of the theory: ...@@ -24,8 +24,8 @@ Changes in and extensions of the theory:
functions. functions.
* [#] Add atomic updates and logically atomic triples, including tactic support. * [#] Add atomic updates and logically atomic triples, including tactic support.
See `heap_lang/lib/increment.v` for an example. See `heap_lang/lib/increment.v` for an example.
* [#] HeapLang now uses right-to-left evaluation order. This makes easier to * [#] HeapLang now uses right-to-left evaluation order. This makes it
write specifications of curried functions. significantly easier to write specifications of curried functions.
Changes in Coq: Changes in Coq:
...@@ -78,6 +78,7 @@ Changes in Coq: ...@@ -78,6 +78,7 @@ Changes in Coq:
* `namespaces` has been moved to std++. * `namespaces` has been moved to std++.
* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and * Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern. changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
* `wp_fork` is now written in curried form.
## Iris 3.1.0 (released 2017-12-19) ## Iris 3.1.0 (released 2017-12-19)
......
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