coqdoc, changelog

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) 

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.