diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2c2be5662ac22a03a9bd94b55855198eee8372e3..8ae1c3de0eaac259ea0b8a2cf6588929a09a2311 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,13 +17,15 @@ Changes in and extensions of the theory:
 * [#] Add weakest preconditions for total program correctness.
 * [#] "(Potentially) stuck" weakest preconditions are no longer considered
   experimental.
+* [#] The adequacy statement for weakest preconditions now also involves the
+  final state.
 * [#] The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   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.
+* [#] heap_lang now uses right-to-left evaluation order. This makes it
+  significantly easier to write specifications of curried functions.
 
 Changes in Coq:
 
@@ -76,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)
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d0f5cffddae4dd32f4af0c050abf69f2a0c7d69f..115ba5c5051fb6b73fa2e8563dc87bb77df85a76 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1395,6 +1395,10 @@ Section option.
       by eapply (cmra_validN_le n); last lia.
     - done.
   Qed.
+
+  Global Instance option_cancelable (ma : option A) :
+    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
+  Proof. destruct ma; apply _. Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 5df537032033b4a7e15be630cdc65ead3b1decc9..59230337296832a37a64068723e2ca9d3970672e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -288,6 +288,12 @@ Proof.
   - by rewrite lookup_singleton_ne // !(left_id None _).
 Qed.
 
+Global Instance gmap_cancelable (m : gmap K A) :
+  (∀ x : A, IdFree x) → (∀ x : A, Cancelable x) → Cancelable m.
+Proof.
+  intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
+Qed.
+
 Lemma insert_op m1 m2 i x y :
   <[i:=x â‹… y]>(m1 â‹… m2) =  <[i:=x]>m1 â‹… <[i:=y]>m2.
 Proof. by rewrite (insert_merge (â‹…) m1 m2 i (x â‹… y) x y). Qed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index aa82505a6e10062d55b81e2d347f36d159f95234..a5f0b688836ee34b189848b05d7444bc9ecb1a32 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -4,6 +4,17 @@ From stdpp Require Export strings.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
+(** heap_lang.  A fairly simple language used for common Iris examples.
+
+- This is a right-to-left evaluated language, like CakeML and OCaml.  The reason
+  for this is that it makes curried functions usable: Given a WP for [f a b], we
+  know that any effects [f] might have to not matter until after *both* [a] and
+  [b] are evaluated.  With left-to-right evaluation, that triple is basically
+  useless the user let-expands [b].
+
+*)
+
+
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.