diff --git a/_CoqProject b/_CoqProject
index 0a711bddc6e25aabb6e9386c7db451033f95041f..071cd83b170d17968892d6a7426f60a2988f83df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -116,7 +116,6 @@ theories/heap_lang/lib/clairvoyant_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
-theories/heap_lang/lib/compare_and_set.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0b4905002c9450b94bcdc45a01dfaf04fb01ac8a..cd0bad54ed33ea83f95f544a5ffe352e8874aa58 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -40,7 +40,7 @@
   ============================
   _ : ▷ l ↦ #0
   --------------------------------------∗
-  WP CAS #l #0 #1 {{ _, l ↦ #1 }}
+  WP CompareExchange #l #0 #1 {{ _, l ↦ #1 }}
   
 1 subgoal
   
@@ -148,4 +148,5 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
      : string
 The command has indeed failed with message:
 Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
+Tactic failure: wp_cas_suc: cannot find 'CompareExchange' in 
+(#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index ebde315ef532338106d2e92fd940d5ec72464eaf..fe19053fb723e2b59fc2db05e0dfdd4e448e0ad3 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -79,7 +79,7 @@ Section tests.
   Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
   Proof. wp_lam. wp_op. by case_bool_decide. Qed.
 
-  Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
+  Definition heap_e7 : val := λ: "v", CompareExchange "v" #0 #1.
 
   Lemma heap_e7_spec_total l : l ↦ #0 -∗ WP heap_e7 #l [{_,  l ↦ #1 }].
   Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
@@ -126,7 +126,7 @@ Section tests.
 
   Lemma wp_cas l v :
     val_is_unboxed v →
-    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
+    l ↦ v -∗ WP CompareExchange #l v v {{ _, True }}.
   Proof.
     iIntros (?) "?". wp_cas as ? | ?. done. done.
   Qed.
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index ce457089e8f009953b4d87b8f004f3e7ebdabfed..7eb5a86b711f6d25d58f98b76fb962da92c2c902 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -11,7 +11,8 @@ Section tests.
   Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
     l ↦ #n -∗
     proph p vs -∗
-    WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #n⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
+    WP Resolve (CompareExchange #l #n (#n + #1)) #p v @ E
+      {{ v, ⌜v = (#true, #n)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
     wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 35b88e56a87c9c4a210f49fbb31c5c6f31580796..d961c559b6c3abbdf72d95bf04f7802201b05d85 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val :=
   rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l".
+    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
 
 (** The CMRA we need. *)
@@ -222,7 +222,7 @@ Section counter_proof.
     iDestruct 1 as (c) "[Hl Hγ]".
     wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     wp_let. wp_op.
-    wp_bind (CAS _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
+    wp_bind (CompareExchange _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c') ">[Hl Hγ]".
     destruct (decide (c' = c)) as [->|].
     - iCombine "Hγ" "Hγf" as "Hγ".
@@ -231,11 +231,10 @@ Section counter_proof.
       rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
       wp_cas_suc. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_op. rewrite bool_decide_true //. wp_if. rewrite {3}/C; eauto 10.
-    - assert (#c ≠ #c') by (intros [=]; abstract omega). wp_cas_fail.
+      wp_pures. rewrite {3}/C; eauto 10.
+    - wp_cas_fail; first (intros [=]; abstract omega).
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_op. rewrite bool_decide_false //. wp_if.
-      iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
+      wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
   Check "read_spec".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e386c7ad4ef1d800d01dfccb44a50a5949ad2846..2c93e917b49dde2540c4cb8dad97a29f900c8f38 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",
-    CAS "x" NONE (SOME "n") = NONE),
+    CAS "x" NONE (SOME "n")),
   (* check  *) (λ: <>,
     let: "y" := !"x" in λ: <>,
     match: "y" with
@@ -49,15 +49,13 @@ Proof.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   wp_pures. iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CAS _ _ _).
+  - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CompareExchange _ _ _).
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
-      wp_cas_suc. iSplitL; iModIntro; last first.
-      { wp_pures. eauto. }
+      wp_cas_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
       iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iSplitL; iModIntro; last first.
-      { wp_pures. eauto. }
+    + wp_cas_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 1521d1d673c7e8c520e58ceee2d24812841290fa..ea963e3eaca56f746a1e41a14a161268ffcbac8d 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -97,7 +97,7 @@ Inductive expr :=
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-and-swap (NOT compare-and-set!) *)
+  | CompareExchange (e0 : expr) (e1 : expr) (e2 : expr)
   | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
@@ -235,7 +235,7 @@ Proof.
      | Load e, Load e' => cast_if (decide (e = e'))
      | Store e1 e2, Store e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
-     | CAS e0 e1 e2, CAS e0' e1' e2' =>
+     | CompareExchange e0 e1 e2, CompareExchange e0' e1' e2' =>
         cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
      | FAA e1 e2, FAA e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
@@ -311,7 +311,7 @@ Proof.
      | AllocN e1 e2 => GenNode 13 [go e1; go e2]
      | Load e => GenNode 14 [go e]
      | Store e1 e2 => GenNode 15 [go e1; go e2]
-     | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
+     | CompareExchange e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
      | FAA e1 e2 => GenNode 17 [go e1; go e2]
      | NewProph => GenNode 18 []
      | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
@@ -346,7 +346,7 @@ Proof.
      | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
      | GenNode 14 [e] => Load (go e)
      | GenNode 15 [e1; e2] => Store (go e1) (go e2)
-     | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
+     | GenNode 16 [e0; e1; e2] => CompareExchange (go e0) (go e1) (go e2)
      | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
      | GenNode 18 [] => NewProph
      | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
@@ -401,9 +401,9 @@ Inductive ectx_item :=
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
-  | CasLCtx (v1 : val) (v2 : val)
-  | CasMCtx (e0 : expr) (v2 : val)
-  | CasRCtx (e0 : expr) (e1 : expr)
+  | CompareExchangeLCtx (v1 : val) (v2 : val)
+  | CompareExchangeMCtx (e0 : expr) (v2 : val)
+  | CompareExchangeRCtx (e0 : expr) (e1 : expr)
   | FaaLCtx (v2 : val)
   | FaaRCtx (e1 : expr)
   | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
@@ -437,9 +437,9 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
-  | CasLCtx v1 v2 => CAS e (Val v1) (Val v2)
-  | CasMCtx e0 v2 => CAS e0 e (Val v2)
-  | CasRCtx e0 e1 => CAS e0 e1 e
+  | CompareExchangeLCtx v1 v2 => CompareExchange e (Val v1) (Val v2)
+  | CompareExchangeMCtx e0 v2 => CompareExchange e0 e (Val v2)
+  | CompareExchangeRCtx e0 e1 => CompareExchange e0 e1 e
   | FaaLCtx v2 => FAA e (Val v2)
   | FaaRCtx e1 => FAA e1 e
   | ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
@@ -468,7 +468,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
   | Load e => Load (subst x v e)
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
-  | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
+  | CompareExchange e0 e1 e2 => CompareExchange (subst x v e0) (subst x v e1) (subst x v e2)
   | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
   | NewProph => NewProph
   | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
@@ -634,13 +634,14 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CasS l v1 v2 vl σ :
+  | CompareExchangeS l v1 v2 vl σ :
      vals_cas_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
-     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
+     (* Crucially, this compares the same way as [EqOp]! *)
+     let b := bool_decide (val_for_compare vl = val_for_compare v1) in
+     head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (* Crucially, this compares the same way as [EqOp]! *)
-               (Val vl) (if decide (val_for_compare vl = val_for_compare v1) then state_upd_heap <[l:=v2]> σ else σ)
+               (Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
                []
   | FaaS l i1 i2 σ :
      σ.(heap) !! l = Some (LitV (LitInt i1)) →
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index da2fd61c465624f428a897114dd37ff7bcaf5cc7..2b5e28cce1cd0e4709df7390bc8c2a42e30a0db3 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -31,12 +31,14 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
   is outside the atomic triple, which makes it much easier to use -- and the
-  spec is still good enough for all our applications. *)
+  spec is still good enough for all our applications.
+  The postcondition deliberately does not use [bool_decide] so that users can
+  [destruct (decide (a = b))] and it will simplify in both places. *)
   cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET v >>>;
+        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
@@ -100,13 +102,13 @@ Section proof.
     <<< ∀ (v : val), l ↦ v >>>
       primitive_cas #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
-        RET v >>>.
+        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
   Proof.
-    iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
+    iIntros (? Φ) "AU". wp_lam. wp_pures. wp_bind (CompareExchange _ _ _).
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
       [wp_cas_suc|wp_cas_fail];
-    iMod ("Hclose" with "H↦") as "HΦ"; done.
+    iMod ("Hclose" with "H↦") as "HΦ"; iModIntro; by wp_pures.
   Qed.
 End proof.
 
diff --git a/theories/heap_lang/lib/compare_and_set.v b/theories/heap_lang/lib/compare_and_set.v
deleted file mode 100644
index daa5f233cf86740238a76babe3ce4f2683c542fc..0000000000000000000000000000000000000000
--- a/theories/heap_lang/lib/compare_and_set.v
+++ /dev/null
@@ -1,28 +0,0 @@
-From iris.heap_lang Require Export lifting notation.
-From iris.program_logic Require Export atomic.
-From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
-
-(* Defines compare-and-set (CASet) on top of compare-and-swap (CAS). *)
-
-Definition compare_and_set : val :=
-  λ: "l" "v1" "v2", CAS "l" "v1" "v2" = "v1".
-
-Section proof.
-  Context `{!heapG Σ}.
-
-  (* This is basically a logically atomic spec, but stronger and hence easier to apply. *)
-  Lemma caset_spec (l : loc) (v1 v2 : val) Φ E :
-    val_is_unboxed v1 →
-    (|={⊤,E}=> ∃ v, l ↦ v ∗ let b := bool_decide (val_for_compare v = val_for_compare v1) in
-        (l ↦ (if b then v2 else v) ={E,⊤}=∗ Φ #b) ) -∗
-    WP compare_and_set #l v1 v2 @ ⊤ {{ Φ }}.
-  Proof.
-    iIntros (?) "AU". wp_lam. wp_pures. wp_bind (CAS _ _ _).
-    iMod "AU" as (v) "[H↦ Hclose]". case_bool_decide.
-    - wp_cas_suc. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
-      rewrite bool_decide_true //.
-    - wp_cas_fail. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
-      rewrite bool_decide_false //.
-  Qed.
-End proof.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8f54eae6ea1a7bfd5cbef70cd99c53b6043efbc4..18a3711881ada6f17276e889ed4ee957d83d03dc 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac_auth auth.
-From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
+From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: compare_and_set "l" "n" (#1 + "n") then #() else "incr" "l".
+    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
@@ -50,25 +50,22 @@ Section mono_proof.
     iDestruct "Hl" as (γ) "[#? Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures. wp_apply caset_spec; first done.
-    iInv N as (c') ">[Hγ Hl]" "Hclose".
+    wp_pures. wp_bind (CompareExchange _ _ _).
+    iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      iExists _; iFrame "Hl". iIntros "!> Hl".
-      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. iFrame. }
-      iModIntro. wp_if.
-      iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
+      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+      wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
       apply: auth_frag_mono. by apply mnat_included, le_n_S.
-    - iExists _; iFrame "Hl". iIntros "!> Hl".
-      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
-      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
+      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
@@ -132,19 +129,17 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures. wp_apply caset_spec; first done.
-    iInv N as (c') ">[Hγ Hl]" "Hclose".
+    wp_pures. wp_bind (CompareExchange _ _ _).
+    iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
-      iExists _; iFrame "Hl". iIntros "!> Hl".
-      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      iModIntro. wp_if. by iApply "HΦ".
-    - iExists _; iFrame "Hl". iIntros "!> Hl".
-      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
-      iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
-      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      wp_pures. by iApply "HΦ".
+    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
+      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
   Lemma read_contrib_spec γ l q n :
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index fd4af19bbf34e67495d5c4265f9bb19a01982158..1fbdea446ca9295ae60cea45d4698c29d17f6b00 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -16,7 +16,7 @@ Section increment_physical.
   Definition incr_phy : val :=
     rec: "incr" "l" :=
        let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
+       if: CAS "l" "oldv" ("oldv" + #1)
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
@@ -26,12 +26,12 @@ Section increment_physical.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
     wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
-    wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
+    wp_pures. wp_bind (CompareExchange _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
     destruct (decide (#v = #w)) as [[= ->]|Hx].
     - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iModIntro. wp_op. rewrite bool_decide_true //. wp_if. done.
+      iModIntro. wp_pures. done.
     - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iModIntro. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
+      iModIntro. wp_pures. iApply "IH". done.
   Qed.
 End increment_physical.
 
@@ -45,7 +45,7 @@ Section increment.
   Definition incr : val :=
     rec: "incr" "l" :=
        let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
+       if: CAS "l" "oldv" ("oldv" + #1)
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
@@ -70,9 +70,9 @@ Section increment.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
     iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iIntros "!>". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
+      iIntros "!>". wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iIntros "!>". wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
+      iIntros "!>". wp_if. iApply "IH". done.
   Qed.
 
   (** A proof of the incr specification that uses lemmas to avoid reasining
@@ -94,9 +94,9 @@ Section increment.
     iIntros "H↦ !>".
     simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
     - iRight. iFrame. iIntros "HΦ !>".
-      wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
+      wp_if. by iApply "HΦ".
     - iLeft. iFrame. iIntros "AU !>".
-      wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
+      wp_if. iApply "IH". done.
   Qed.
 
   (** A "weak increment": assumes that there is no race *)
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 2c46b44321d814b37d9a015a2b9be9f89c910d22..36ed310dbb34d7272ac7664f0dcd792b85bad077 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock.
 Set Default Proof Using "Type".
 
 Definition newlock : val := λ: <>, ref #false.
-Definition try_acquire : val := λ: "l", CAS "l" #false #true = #false.
+Definition try_acquire : val := λ: "l", CAS "l" #false #true.
 Definition acquire : val :=
   rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
 Definition release : val := λ: "l", "l" <- #false.
@@ -61,7 +61,7 @@ Section proof.
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. wp_bind (CAS _ _ _). iInv N as ([]) "[Hl HR]".
+    wp_rec. wp_bind (CompareExchange _ _ _). iInv N as ([]) "[Hl HR]".
     - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
       wp_pures. iApply ("HΦ" $! false). done.
     - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index bf0d42dc0fcf69094903010ed50db23515875495..7042cbace817c81d3da9e6355e98cced2aa22ac2 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -20,7 +20,7 @@ Definition newlock : val :=
 Definition acquire : val :=
   rec: "acquire" "lk" :=
     let: "n" := !(Snd "lk") in
-    if: CAS (Snd "lk") "n" ("n" + #1) = "n"
+    if: CAS (Snd "lk") "n" ("n" + #1)
       then wait_loop "n" "lk"
       else "acquire" "lk".
 
@@ -111,7 +111,7 @@ Section proof.
     iInv N as (o n) "[Hlo [Hln Ha]]".
     wp_load. iModIntro. iSplitL "Hlo Hln Ha".
     { iNext. iExists o, n. by iFrame. }
-    wp_pures. wp_bind (CAS _ _ _).
+    wp_pures. wp_bind (CompareExchange _ _ _).
     iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
     destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
     - iMod (own_update with "Hauth") as "[Hauth Hofull]".
@@ -122,14 +122,14 @@ Section proof.
       wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      wp_op. rewrite bool_decide_true //. wp_if.
+      wp_pures.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
       + by iNext.
     - wp_cas_fail. iModIntro.
       iSplitL "Hlo' Hln' Hauth Haown".
       { iNext. iExists o', n'. by iFrame. }
-      wp_op. rewrite bool_decide_false //. wp_if. by iApply "IH"; auto.
+      wp_pures. by iApply "IH"; auto.
   Qed.
 
   Lemma release_spec γ lk R :
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 0db501672964f35dc735e9368a8ab8d1b385047a..f7abd0bb6aa1d835804595c6c2ae7d79f7312675 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -56,7 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
 
 (* [simpl apply] is too stupid, so we need extern hints here. *)
 Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
-Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasS : core.
+Local Hint Extern 0 (head_step (CompareExchange _ _ _) _ _ _ _ _) => eapply CompareExchangeS : core.
 Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
 Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
 Local Hint Resolve to_of_val : core.
@@ -77,7 +77,7 @@ Instance load_atomic s v : Atomic s (Load (Val v)).
 Proof. solve_atomic. Qed.
 Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
-Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
+Instance cas_atomic s v0 v1 v2 : Atomic s (CompareExchange (Val v0) (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
 Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
@@ -376,44 +376,48 @@ Qed.
 
 Lemma wp_cas_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  {{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET v'; l ↦{q} v' }}}.
+  {{{ ▷ l ↦{q} v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET (#false, v'); l ↦{q} v' }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  rewrite /b bool_decide_false //.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  [[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET v'; l ↦{q} v' }]].
+  [[{ l ↦{q} v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET (#false, v'); l ↦{q} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  rewrite /b bool_decide_false //.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  {{{ ▷ l ↦ v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET v'; l ↦ v2 }}}.
+  {{{ ▷ l ↦ v' }}} CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  {{{ RET (#true, v'); l ↦ v2 }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  rewrite /b bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
-  [[{ l ↦ v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET v'; l ↦ v2 }]].
+  [[{ l ↦ v' }]] CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+  [[{ RET (#true, v'); l ↦ v2 }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  rewrite /b bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -532,8 +536,8 @@ Qed.
 Lemma wp_resolve_cas_suc s E (l : loc) (p : proph_id) (pvs : list (val * val)) (v1 v2 v : val) :
   vals_cas_compare_safe v1 v1 →
   {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
-    Resolve (CAS #l v1 v2) #p v @ s; E
-  {{{ RET v1 ; ∃ pvs', ⌜pvs = (v1, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
+    Resolve (CompareExchange #l v1 v2) #p v @ s; E
+  {{{ RET (#true, v1) ; ∃ pvs', ⌜pvs = ((#true, v1)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
 Proof.
   iIntros (Hcmp Φ) "[Hp Hl] HΦ".
   iApply (wp_resolve with "Hp"); first done.
@@ -545,8 +549,8 @@ Qed.
 Lemma wp_resolve_cas_fail s E (l : loc) (p : proph_id) (pvs : list (val * val)) q (v' v1 v2 v : val) :
   val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
   {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
-    Resolve (CAS #l v1 v2) #p v @ s; E
-  {{{ RET v' ; ∃ pvs', ⌜pvs = (v', v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+    Resolve (CompareExchange #l v1 v2) #p v @ s; E
+  {{{ RET (#false, v') ; ∃ pvs', ⌜pvs = ((#false, v')%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
 Proof.
   iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
   iApply (wp_resolve with "Hp"); first done.
@@ -603,8 +607,8 @@ Lemma wp_cas_suc_offset s E l off vs v' v1 v2 :
   val_for_compare v' = val_for_compare v1 →
   vals_cas_compare_safe v' v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET v'; l ↦∗ <[off:=v2]> vs }}}.
+    CompareExchange #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (#true, v'); l ↦∗ <[off:=v2]> vs }}}.
 Proof.
   iIntros (Hlookup ?? Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -616,8 +620,8 @@ Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
   val_for_compare (vs !!! off) = val_for_compare v1 →
   vals_cas_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (vs !!! off); l ↦∗ vinsert off v2 vs }}}.
+    CompareExchange #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (#true, vs !!! off); l ↦∗ vinsert off v2 vs }}}.
 Proof.
   intros. setoid_rewrite vec_to_list_insert. eapply wp_cas_suc_offset=> //.
   by apply vlookup_lookup.
@@ -628,8 +632,8 @@ Lemma wp_cas_fail_offset s E l off vs v0 v1 v2 :
   val_for_compare v0 ≠ val_for_compare v1 →
   vals_cas_compare_safe v0 v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET v0; l ↦∗ vs }}}.
+    CompareExchange #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (#false, v0); l ↦∗ vs }}}.
 Proof.
   iIntros (Hlookup HNEq Hcmp Φ) ">Hl HΦ".
   iDestruct (update_array l _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -643,8 +647,8 @@ Lemma wp_cas_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
   val_for_compare (vs !!! off) ≠ val_for_compare v1 →
   vals_cas_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CAS #(l +â‚— off) v1 v2 @ s; E
-  {{{ RET (vs !!! off); l ↦∗ vs }}}.
+    CompareExchange #(l +â‚— off) v1 v2 @ s; E
+  {{{ RET (#false, vs !!! off); l ↦∗ vs }}}.
 Proof. intros. eapply wp_cas_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index a8b565813fc1bcc2788ad7611f1e738c65db1e67..a4b667f6b7ac46d3e4fc1042f597a983612e8b8c 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -14,7 +14,7 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
      is_closed_expr X e
   | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
-  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 | Resolve e0 e1 e2 =>
+  | If e0 e1 e2 | Case e0 e1 e2 | CompareExchange e0 e1 e2 | Resolve e0 e1 e2 =>
      is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
   | NewProph => true
   end
@@ -170,7 +170,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
-  | CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
+  | CompareExchange e0 e1 e2 => CompareExchange (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
   | NewProph => NewProph
   | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 204ec38ab76de2a755935bfdb13ef8a68350bb96..f926a7e85fa62be23ec141a1e4280910de7e531f 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -25,6 +25,7 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
 Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
 Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
+Notation CAS l e1 e2 := (Fst (CompareExchange l e1 e2)) (only parsing).
 
 (* Skip should be atomic, we sometimes open invariants around
    it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 352607d1d674a54481c3a2a6e2ee68d39a72d0ac..77acaed176cea4e97a915345044cc335549c9247 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -284,10 +284,10 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   vals_cas_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }})) →
+   envs_entails Δ'' (WP fill K (Val (#true, v)) @ s; E {{ Φ }})) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
+   envs_entails Δ' (WP fill K (Val (#false, v)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ???? Hsuc Hfail.
   destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
@@ -305,10 +305,10 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   vals_cas_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }])) →
+   envs_entails Δ' (WP fill K (Val (#true, v)) @ s; E [{ Φ }])) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }])) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+   envs_entails Δ (WP fill K (Val (#false, v)) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ??? Hsuc Hfail.
   destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
@@ -326,8 +326,8 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Val (#false, v)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ?????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
@@ -337,8 +337,8 @@ Qed.
 Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
   val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+  envs_entails Δ (WP fill K (Val (#false, v)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
   eapply wand_apply; first exact: twp_cas_fail.
@@ -350,8 +350,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Val (#true, v)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??????; subst.
   rewrite -wp_bind. eapply wand_apply.
@@ -363,8 +363,8 @@ Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }]) →
-  envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
+  envs_entails Δ' (WP fill K (Val (#true, v)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CompareExchange (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=>?????; subst.
   rewrite -twp_bind. eapply wand_apply.
@@ -545,7 +545,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas _ _ _ _ _ _ K))
-      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas: cannot find 'CompareExchange' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
@@ -555,7 +555,7 @@ Tactic Notation "wp_cas" "as" simple_intropattern(H1) "|" simple_intropattern(H2
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas _ _ _ _ _ K))
-      |fail 1 "wp_cas: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas: cannot find 'CompareExchange' in" e];
     [solve_mapsto ()
     |pm_reflexivity
     |try solve_vals_cas_compare_safe
@@ -573,7 +573,7 @@ Tactic Notation "wp_cas_fail" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_fail _ _ _ _ _ K))
-      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas_fail: cannot find 'CompareExchange' in" e];
     [iSolveTC
     |solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
@@ -582,7 +582,7 @@ Tactic Notation "wp_cas_fail" :=
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
-      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas_fail: cannot find 'CompareExchange' in" e];
     [solve_mapsto ()
     |try (simpl; congruence) (* value inequality *)
     |try solve_vals_cas_compare_safe
@@ -599,7 +599,7 @@ Tactic Notation "wp_cas_suc" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_cas_suc _ _ _ _ _ _ K))
-      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas_suc: cannot find 'CompareExchange' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
@@ -609,7 +609,7 @@ Tactic Notation "wp_cas_suc" :=
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
-      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+      |fail 1 "wp_cas_suc: cannot find 'CompareExchange' in" e];
     [solve_mapsto ()
     |pm_reflexivity
     |try (simpl; congruence) (* value equality *)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 6ea6feb75b0d4041d54b3f70c8612c7858994dd3..041e36f32c5e5695c72d6b336f437df3f14fba47 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -35,9 +35,12 @@ Ltac reshape_expr e tac :=
     | Load ?e                         => add_item LoadCtx vs K e
     | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
     | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2
-    | CAS ?e0 (Val ?v1) (Val ?v2)     => add_item (CasLCtx v1 v2) vs K e0
-    | CAS ?e0 ?e1 (Val ?v2)           => add_item (CasMCtx e0 v2) vs K e1
-    | CAS ?e0 ?e1 ?e2                 => add_item (CasRCtx e0 e1) vs K e2
+    | CompareExchange ?e0 (Val ?v1) (Val ?v2)
+                                      => add_item (CompareExchangeLCtx v1 v2) vs K e0
+    | CompareExchange ?e0 ?e1 (Val ?v2)
+                                      => add_item (CompareExchangeMCtx e0 v2) vs K e1
+    | CompareExchange ?e0 ?e1 ?e2
+                                      => add_item (CompareExchangeRCtx e0 e1) vs K e2
     | FAA ?e (Val ?v)                 => add_item (FaaLCtx v) vs K e
     | FAA ?e1 ?e2                     => add_item (FaaRCtx e1) vs K e2
     | Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex