diff --git a/CHANGELOG.md b/CHANGELOG.md
index 914e342653d36c58cac59a6ea5279a05805b921b..ec79d1b6ab87c3f5c0305a000c424cc844a74e58 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,10 @@ lemma.
 * Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
   non-atomic invariant tokens. (by Benjamin Peters)
 
+**Changes in `heap_lang`:**
+
+* Make `wp_cmpxchg_fail` work when the points-to is in the persistent context.
+
 **Infrastructure:**
 
 * Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5ff0afe4d2a35d7e5b6a1d8be5feaae9ab3f83a1..b8d209d82bcfd5281b264cff7988880445a40b64 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -410,12 +410,14 @@ Section pointsto_tests.
     iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
   Qed.
 
-  (* Failing CmpXchg from a persistent points-to predicate in the _persistent_ context. *)
+  (* Failing [CmpXchg] from a persistent points-to predicate in the _persistent_
+  context. *)
   Lemma persistent_pointsto_cmpxchg_persistent l :
     {{{ l ↦□ #1 }}} CmpXchg #l #0 #1 {{{ v, RET v; True }}}.
   Proof. iIntros (Φ) "#Hl HΦ". wp_cmpxchg_fail. by iApply "HΦ". Qed.
 
-  (* Failing CmpXchg from a persistent points-to predicate in the _spatial_ context. *)
+  (* Failing [CmpXchg] from a persistent points-to predicate in the _spatial_
+  context. *)
   Lemma persistent_pointsto_cmpxchg_spatial l :
     {{{ l ↦□ #1 }}} CmpXchg #l #0 #1 {{{ v, RET v; True }}}.
   Proof. iIntros (Φ) "Hl HΦ". wp_cmpxchg_fail. by iApply "HΦ". Qed.