diff --git a/CHANGELOG.md b/CHANGELOG.md index e3890924d111d5e183f060b4ea0e80928488de6e..d93f562fe8c5c4e960d535a734f09cb29e923803 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,8 +24,8 @@ Changes in and extensions of the theory: functions. * [#] Add atomic updates and logically atomic triples, including tactic support. See `heap_lang/lib/increment.v` for an example. -* [#] HeapLang now uses right-to-left evaluation order. This makes easier to - write specifications of curried functions. +* [#] HeapLang now uses right-to-left evaluation order. This makes it + significantly easier to write specifications of curried functions. Changes in Coq: @@ -78,6 +78,7 @@ Changes in Coq: * `namespaces` has been moved to std++. * 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. +* `wp_fork` is now written in curried form. ## Iris 3.1.0 (released 2017-12-19)