diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 6faabec4d18e7c9b4fa03d21eec57a2b6de2cbab..535405737525a9aba2866dcb81e4c7b639026285 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-09-14.3.60632dd7") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-09-26.0.32e79061") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index e650008a3b34f5059f1e0513d94c133358eeb3cd..97e795fba7e4352a974ef2de50aa2322f3c2038d 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -44,9 +44,9 @@ Section tada.
     else True.
 
   Local Definition acquire_AU γ (Q : iProp Σ) : iProp Σ :=
-    AU << ∃∃ s : state, tada_lock_state γ s >>
+    AU <{ ∃∃ s : state, tada_lock_state γ s }>
        @ ⊤ ∖ ↑N, ∅
-       << tada_lock_state γ Locked, COMM Q >>.
+       <{ tada_lock_state γ Locked, COMM Q }>.
 
   Local Instance acquire_AU_proper γ :
     NonExpansive (acquire_AU γ).
@@ -197,9 +197,9 @@ Section tada.
   Lemma acquire_tada_spec γ lk :
     tada_is_lock γ lk -∗
     £2 -∗
-    <<< ∀∀ s, tada_lock_state γ s >>>
+    <<{ ∀∀ s, tada_lock_state γ s }>>
       l.(acquire) lk @ ↑N
-    <<< tada_lock_state γ Locked, RET #() >>>.
+    <<{ tada_lock_state γ Locked | RET #() }>>.
   Proof.
     iIntros "[#Hislock #Hinv] [Hlc1 Hlc2] %Φ AU".
     iMod (register_lock_acquire with "Hinv AU") as (q) "[Hown Hloan]".
@@ -218,9 +218,9 @@ Section tada.
 
   Lemma release_tada_spec γ lk :
     tada_is_lock γ lk -∗
-    <<< tada_lock_state γ Locked >>>
+    <<{ tada_lock_state γ Locked }>>
       l.(release) lk @ ↑N
-    <<< tada_lock_state γ Free, RET #() >>>.
+    <<{ tada_lock_state γ Free | RET #() }>>.
   Proof.
     iIntros "[#Hislock _] %Φ AU". iApply fupd_wp.
     iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index c16e64823eadb790d693d0122ffafda161bd204c..4c65e63ee3f385ce8098e4ddfa19c099144396d6 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -184,9 +184,9 @@ Section conditional_counter.
        ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state Q l l_ghost_winner γ_t))%I.
 
   Local Definition cinc_au Q γs f :=
-    (AU << ∃∃ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>
+    (AU <{ ∃∃ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>
            @ ⊤∖(↑N ∪ ↑inv_heapN), ∅
-        << counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, COMM Q >>)%I.
+        <{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, COMM Q }>)%I.
 
   Definition counter_inv γ_n c :=
     (∃ (l : loc) (q : Qp) (s : abstract_state),
@@ -432,9 +432,9 @@ Section conditional_counter.
 
   Lemma cinc_spec γs v (f: loc) :
     is_counter γs v -∗
-    <<< ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>>
+    <<{ ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>>
         cinc v #f @ (↑N ∪ ↑inv_heapN)
-    <<< counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, RET #() >>>.
+    <<{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b | RET #() }>>.
   Proof.
     iIntros "#InvC". iDestruct "InvC" as (c_l [-> ?]) "[#GC #InvC]".
     iIntros (Φ) "AU". iLöb as "IH".
@@ -515,9 +515,9 @@ Section conditional_counter.
 
   Lemma get_spec γs v :
     is_counter γs v -∗
-    <<< ∀∀ (n : Z), counter_content γs n >>>
+    <<{ ∀∀ (n : Z), counter_content γs n }>>
         get v @ (↑N ∪ ↑inv_heapN)
-    <<< counter_content γs n, RET #n >>>.
+    <<{ counter_content γs n | RET #n }>>.
   Proof.
     iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (c_l [-> ?]) "[GC InvC]".
     iLöb as "IH". wp_lam. wp_bind (! _)%E.
diff --git a/theories/logatom/conditional_increment/spec.v b/theories/logatom/conditional_increment/spec.v
index 501a3e18b5402ede92f6a9dccd874ee6db92c080..15a03266c639912af1811c5e3b2946958f92c4f9 100644
--- a/theories/logatom/conditional_increment/spec.v
+++ b/theories/logatom/conditional_increment/spec.v
@@ -31,14 +31,14 @@ Record atomic_cinc {Σ} `{!heapGS Σ} := AtomicCinc {
     {{{ ctr γs, RET ctr ; is_counter N γs ctr ∗ counter_content γs 0 }}};
   cinc_spec N γs v (f : loc) :
     is_counter N γs v -∗
-    <<< ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>>
+    <<{ ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>>
         cinc v #f @ ↑N ∪ ↑inv_heapN
-    <<< counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, RET #() >>>;
+    <<{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b | RET #() }>>;
   get_spec N γs v:
     is_counter N γs v -∗
-    <<< ∀∀ (n : Z), counter_content γs n >>>
+    <<{ ∀∀ (n : Z), counter_content γs n }>>
         get v @ ↑N ∪ ↑inv_heapN
-    <<< counter_content γs n, RET #n >>>;
+    <<{ counter_content γs n | RET #n }>>;
 }.
 Global Arguments atomic_cinc _ {_}.
 
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 40c100089954bc7621ed0a0e3dc413500e3dfc6c..7c1ec6cbafa97d372fa3ed7d329330f314385d14 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -105,12 +105,12 @@ Section counter_proof.
 
   (** Invariant for transfer of atomic update (helping) of [get] *)
   Definition get_inv γs (γ1 γ2 : gname) (n : nat) (Φ : val → iProp Σ) : iProp Σ :=
-    ((AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs n, COMM (Φ #n) >> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
+    ((AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs n, COMM (Φ #n) }> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
      (ghost_var γ1 (1/2) false ∗ Φ #n) ∨ (ghost_var γ1 (1/2) false ∗ own γ2 (Excl ()))).
 
   (** Invariant for transfer of atomic update (helping) of [put] *)
   Definition put_inv γs (γ1 γ2 : gname) (n : nat) (Φ : val → iProp Σ): iProp Σ :=
-    ((AU  << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs (n + 1), COMM (Φ #n) >> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
+    ((AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs (n + 1), COMM (Φ #n) }> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
      (ghost_var γ1 (1/2) false ∗ Φ #n) ∨ (ghost_var γ1 (1/2) false ∗ own γ2 (Excl ()))).
 
   (** The part of the main counter invariant that controls execution of [put]s *)
@@ -307,7 +307,7 @@ Section counter_proof.
 
   Lemma counter_inv_inner_register_get Φ E γs γ_prim γ_get γ_put γ b p G P n_b n_p :
     n_b < n_p →
-    AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs n, COMM (Φ #n) >> -∗
+    AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs n, COMM (Φ #n) }> -∗
     £ 1 -∗
     n_p ↪[ γ_get ]□ γ -∗
     counter_inv_inner γs γ_prim γ_get γ_put b p G P n_b n_p ={E}=∗
@@ -348,7 +348,7 @@ Section counter_proof.
 
   Lemma counter_inv_inner_register_put Φ E γs γ_prim γ_get γ_put b p G P n_b n_p :
     n_b ≤ n_p →
-    AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs (n + 1), COMM (Φ #n) >> -∗
+    AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs (n + 1), COMM (Φ #n) }> -∗
     £ 1 -∗
     b ↦ #n_b -∗
     p ↦ #(S n_p) -∗
@@ -530,7 +530,7 @@ Section counter_proof.
 
   (** *** Proof of [get] *)
   Lemma get_spec γs (c : val) :
-    is_counter γs c -∗ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n : nat), value γs n }>> (get c) @ ↑N <<{ value γs n | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -568,7 +568,7 @@ Section counter_proof.
 
   (** *** Proof of [get_backup] *)
   Lemma get_backup_spec γs (c: val) :
-    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n: nat), value γs n }>> (get_backup c) @ ↑N <<{ value γs n | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -589,7 +589,7 @@ Section counter_proof.
 
   (** *** Proof of [increment] *)
   Lemma increment_spec γs (c: val) :
-    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n: nat), value γs n }>> (increment c) @ ↑N <<{ value γs (n + 1) | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
diff --git a/theories/logatom/counter_with_backup/counter_spec.v b/theories/logatom/counter_with_backup/counter_spec.v
index 4ded0004d5212fc82039bfa2a3a7160438b54d5c..d7936969a38517b4da8d8266c6bda8ca0078afb1 100644
--- a/theories/logatom/counter_with_backup/counter_spec.v
+++ b/theories/logatom/counter_with_backup/counter_spec.v
@@ -24,22 +24,22 @@ Record atomic_counter {Σ} `{!heapGS Σ} := AtomicCounter {
   (* -- operation specs -- *)
   new_counter_spec N :
     {{{ True }}} new_counter #() {{{ c γs, RET c; is_counter N γs c ∗ value γs 0 }}};
-  (* the following specs are logically atomic, using logically-atomic triples <<< x. P >>> e <<< y. Q >>> *)
+  (* the following specs are logically atomic, using logically-atomic triples <<{ x. P }>> e <<{ y. Q }>> *)
   (* note that the [RET] clause _specifies_ that the return value is [n], and hence we do not need to introduce a separate binder [m] as is done in the formulation shown in the paper *)
   increment_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       increment c @ ↑N
-    <<< value γs (n + 1), RET #n >>>;
+    <<{ value γs (n + 1) | RET #n }>>;
   get_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       get c @ ↑N
-    <<< value γs n, RET #n >>>;
+    <<{ value γs n | RET #n }>>;
   get_backup_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       get_backup c @ ↑N
-    <<< value γs n, RET #n >>>;
+    <<{ value γs n | RET #n }>>;
 }.
 Global Arguments atomic_counter _ {_}.
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index d476906e24324c11333b7d3dc75acac33d38ef1d..b08dbe29fa3d933b6b968b6ac913fe35d0ffb50d 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -166,9 +166,9 @@ Section hocap_auth_tada.
 
   Lemma tada_push N γs s (v : val) :
     stack.(hocap_auth.is_stack) N γs s -∗
-    <<< ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l >>>
+    <<{ ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l }>>
       stack.(hocap_auth.push) s v @ ↑N
-    <<< stack.(hocap_auth.stack_content_frag) γs (v::l), RET #() >>>.
+    <<{ stack.(hocap_auth.stack_content_frag) γs (v::l) | RET #() }>>.
   Proof.
     iIntros "Hstack". iIntros (Φ) "HΦ".
     iApply (hocap_auth.push_spec with "Hstack").
@@ -181,10 +181,10 @@ Section hocap_auth_tada.
 
   Lemma tada_pop N γs (s : val) :
     stack.(hocap_auth.is_stack) N γs s -∗
-    <<< ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l >>>
+    <<{ ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l }>>
       stack.(hocap_auth.pop) s @ ↑N
-    <<< stack.(hocap_auth.stack_content_frag) γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+    <<{ stack.(hocap_auth.stack_content_frag) γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>.
   Proof.
     iIntros "Hstack". iIntros (Φ) "HΦ".
     iApply (hocap_auth.pop_spec with "Hstack").
diff --git a/theories/logatom/elimination_stack/spec.v b/theories/logatom/elimination_stack/spec.v
index 3ae43c10b0ee5810e3260717fc560aac73548839..063eec6770279ae58d41c3ff25b87953f88e7a3c 100644
--- a/theories/logatom/elimination_stack/spec.v
+++ b/theories/logatom/elimination_stack/spec.v
@@ -25,15 +25,15 @@ Record atomic_stack {Σ} `{!heapGS Σ} := AtomicStack {
     {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}};
   push_spec N γs s (v : val) :
     is_stack N γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       push s v @ ↑N
-    <<< stack_content γs (v::l), RET #() >>>;
+    <<{ stack_content γs (v::l) | RET #() }>>;
   pop_spec N γs s :
     is_stack N γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       pop s @ ↑N
-    <<< stack_content γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>;
+    <<{ stack_content γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>;
 }.
 Global Arguments atomic_stack _ {_}.
 
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index d48aa0bc0c92329f3762e8e24c67c15744b85607..72bf3df9a34b7b7de745ac8b534e2c64af3abe17 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -142,7 +142,7 @@ Section stack.
   Local Hint Extern 0 (environments.envs_entails _ (offer_inv _ _ _ _)) => unfold offer_inv : core.
 
   Definition stack_push_au γs v Q : iProp :=
-    AU << ∃∃ l, stack_content γs l >> @ ⊤∖↑N, ∅ << stack_content γs (v::l), COMM Q >>.
+    AU <{ ∃∃ l, stack_content γs l }> @ ⊤∖↑N, ∅ <{ stack_content γs (v::l), COMM Q }>.
 
   Definition is_offer (γs : gname) (offer_rep : option (val * loc)) :=
     match offer_rep with
@@ -187,9 +187,9 @@ Section stack.
 
   Lemma push_spec γs s (v : val) :
     is_stack γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       push s v @ ↑N
-    <<< stack_content γs (v::l), RET #() >>>.
+    <<{ stack_content γs (v::l) | RET #() }>>.
   Proof.
     iIntros "#Hinv". iIntros (Φ) "AU".
     iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
@@ -270,10 +270,10 @@ Section stack.
 
   Lemma pop_spec γs (s : val) :
     is_stack γs s -∗
-    <<< ∀∀ l, stack_content γs l >>>
+    <<{ ∀∀ l, stack_content γs l }>>
       pop s @ ↑N
-    <<< stack_content γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+    <<{ stack_content γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>.
   Proof.
     iIntros "#Hinv". iIntros (Φ) "AU".
     iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v
index 8b423c7252f0c6143365ed175567a0d400460afa..d67e510cdc92cf182ec211ad6a3540695cb4d884 100644
--- a/theories/logatom/flat_combiner/atomic_sync.v
+++ b/theories/logatom/flat_combiner/atomic_sync.v
@@ -29,7 +29,7 @@ Section atomic_sync.
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=
     (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x →
-       <<< ∀∀ g, gHalf γ g ∗ □ α g >>> f' x @ ∅ <<< ∃∃ v g', gHalf γ g' ∗ β g g' v, RET v >>>)%I.
+       <<{ ∀∀ g, gHalf γ g ∗ □ α g }>> f' x @ ∅ <<{ ∃∃ v g', gHalf γ g' ∗ β g g' v | RET v }>>)%I.
 
   (* TODO: Use our usual style with a generic post-condition. *)
   (* TODO: We could get rid of the x, and hard-code a unit. That would
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index caee2fbcff85ff81218e065916ace6f5a98d3583..3b463cdbbc9129588e1a6a609986b87658b6ac62 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1208,8 +1208,8 @@ Qed.
 
 (** Atomic update for the insertion of [l], with post-condition [Q]. *)
 Definition enqueue_AU γe l Q :=
-  (AU << ∃∃ ls : list loc, hwq_cont γe ls >> @ ⊤ ∖ ↑N, ∅
-      << hwq_cont γe (ls ++ [l]), COMM Q >>)%I.
+  (AU <{ ∃∃ ls : list loc, hwq_cont γe ls }> @ ⊤ ∖ ↑N, ∅
+      <{ hwq_cont γe (ls ++ [l]), COMM Q }>)%I.
 
 (*
 When a contradiction is going on, we have [cont = WithCont i1 i2] where:
@@ -1528,9 +1528,9 @@ Qed.
 
 Lemma enqueue_spec sz γe (q : val) (l : loc) :
   is_hwq sz γe q -∗
-  <<< ∀∀ (ls : list loc), hwq_cont γe ls >>>
+  <<{ ∀∀ (ls : list loc), hwq_cont γe ls }>>
     enqueue q #l @ ↑N
-  <<< hwq_cont γe (ls ++ [l]), RET #() >>>.
+  <<{ hwq_cont γe (ls ++ [l]) | RET #() }>>.
 Proof.
   iIntros "Hq" (Φ) "AU".
   iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
@@ -2497,9 +2497,9 @@ Qed.
 
 Lemma dequeue_spec sz γe (q : val) :
   is_hwq sz γe q -∗
-  <<< ∀∀ (ls : list loc), hwq_cont γe ls >>>
+  <<{ ∀∀ (ls : list loc), hwq_cont γe ls }>>
     dequeue q @ ↑N
-  <<< ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_cont γe ls', RET #l >>>.
+  <<{ ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_cont γe ls' | RET #l }>>.
 Proof.
   iIntros "Hq" (Φ) "AU". iLöb as "IH".
   iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
diff --git a/theories/logatom/herlihy_wing_queue/spec.v b/theories/logatom/herlihy_wing_queue/spec.v
index ec760f43985ba3be33bb7d0202ca6e8a3cd0a79f..88cbb80f95af9a7b01dcbfaaff72e17b7bf4ce39 100644
--- a/theories/logatom/herlihy_wing_queue/spec.v
+++ b/theories/logatom/herlihy_wing_queue/spec.v
@@ -28,14 +28,14 @@ Record atomic_hwq {Σ} `{!heapGS Σ} := AtomicHWQ {
     {{{ v γ, RET v; is_hwq N sz γ v ∗ hwq_content γ [] }}};
   enqueue_spec N (sz : nat) (γ : name) (q : val) (l : loc) :
     is_hwq N sz γ q -∗
-    <<< ∀∀ (ls : list loc), hwq_content γ ls >>>
+    <<{ ∀∀ (ls : list loc), hwq_content γ ls }>>
       enqueue q #l @ ↑N
-    <<< hwq_content γ (ls ++ [l]), RET #() >>>;
+    <<{ hwq_content γ (ls ++ [l]) | RET #() }>>;
   dequeue_spec N (sz : nat) (γ : name) (q : val) :
     is_hwq N sz γ q -∗
-    <<< ∀∀ (ls : list loc), hwq_content γ ls >>>
+    <<{ ∀∀ (ls : list loc), hwq_content γ ls }>>
       dequeue q @ ↑N
-    <<< ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls', RET #l >>>;
+    <<{ ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls' | RET #l }>>;
 }.
 Global Arguments atomic_hwq _ {_}.
 
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 4050d8bc3b95944f3a8fb7624cdd85a7db34ee80..f18b0726030faab4d981bd7627bb57ea19fd7f2a 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -285,10 +285,10 @@ Section rdcss.
   Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv : core.
 
   Definition rdcss_au Q l_n l_m m1 n1 n2 :=
-    (AU << ∃∃ (m n : val), (l_m ↦_(λ _, True) m) ∗ rdcss_state l_n n >>
+    (AU <{ ∃∃ (m n : val), (l_m ↦_(λ _, True) m) ∗ rdcss_state l_n n }>
          @ ⊤∖(↑N ∪ ↑inv_heapN), ∅
-        << (l_m ↦_(λ _, True) m) ∗ (rdcss_state l_n (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
-           COMM Q n >>)%I.
+        <{ (l_m ↦_(λ _, True) m) ∗ (rdcss_state l_n (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
+           COMM Q n }>)%I.
 
   Definition rdcss_inv l_n :=
     (∃ (s : abstract_state),
@@ -556,9 +556,9 @@ Section rdcss.
     val_is_unboxed m1 →
     val_is_unboxed (InjLV n1) →
     is_rdcss l_n -∗
-    <<< ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state l_n n >>>
+    <<{ ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state l_n n }>>
         rdcss #l_m #l_n m1 n1 n2 @ ↑N ∪ ↑inv_heapN
-    <<< l_m ↦_(λ _, True) m ∗ rdcss_state l_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET n >>>.
+    <<{ l_m ↦_(λ _, True) m ∗ rdcss_state l_n (if decide (m = m1 ∧ n = n1) then n2 else n) | RET n }>>.
   Proof.
     iIntros (Hm1_unbox Hn1_unbox) "(#InvR & #InvGC & %)". iIntros (Φ) "AU".
     (* allocate fresh descriptor *)
@@ -654,9 +654,9 @@ Section rdcss.
   (** ** Proof of [get] *)
   Lemma get_spec l_n :
     is_rdcss l_n -∗
-    <<< ∀∀ (n : val), rdcss_state l_n n >>>
+    <<{ ∀∀ (n : val), rdcss_state l_n n }>>
         get #l_n @↑N
-    <<< rdcss_state l_n n, RET n >>>.
+    <<{ rdcss_state l_n n | RET n }>>.
   Proof.
     iIntros "(#InvR & #InvGC & %)" (Φ) "AU". iLöb as "IH".
     wp_lam. wp_bind (! _)%E. iInv rdcssN as (s) "(>Hln & Hrest)". wp_load.
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
index ddb035bf4f83da4860cf7dc6792c6c013e00900a..587ad42ac499aff450c8cbe5fd3254b38ef7deaa 100644
--- a/theories/logatom/rdcss/spec.v
+++ b/theories/logatom/rdcss/spec.v
@@ -37,14 +37,14 @@ Record atomic_rdcss {Σ} `{!heapGS Σ} := AtomicRdcss {
     val_is_unboxed m1 →
     val_is_unboxed (InjLV n1) →
     is_rdcss N l_n -∗
-    <<< ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state N l_n n >>>
+    <<{ ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state N l_n n }>>
         rdcss #l_m #l_n m1 n1 n2 @ ↑N ∪ ↑inv_heapN
-    <<< l_m ↦_(λ _, True) m ∗ rdcss_state N l_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET n >>>;
+    <<{ l_m ↦_(λ _, True) m ∗ rdcss_state N l_n (if decide (m = m1 ∧ n = n1) then n2 else n) | RET n }>>;
   get_spec N (l_n : loc):
     is_rdcss N l_n -∗
-    <<< ∀∀ (n : val), rdcss_state N l_n n >>>
+    <<{ ∀∀ (n : val), rdcss_state N l_n n }>>
         get #l_n @ ↑N
-    <<< rdcss_state N l_n n, RET n >>>;
+    <<{ rdcss_state N l_n n | RET n }>>;
 }.
 Global Arguments atomic_rdcss _ {_}.
 
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 9152f90da85e13986627a6b3693999a2ef5008b9..e9d2292481bb0f50718645ea1b51a5b37d2935df 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -208,9 +208,9 @@ Section atomic_snapshot.
 
   Lemma write_spec γ (x2: val) p :
       is_snapshot γ p  -∗
-      <<< ∀∀ x : val, snapshot_content γ x >>>
+      <<{ ∀∀ x : val, snapshot_content γ x }>>
         write p x2 @ ↑N
-      <<< snapshot_content γ x2, RET #() >>>.
+      <<{ snapshot_content γ x2 | RET #() }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
     iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
@@ -267,9 +267,9 @@ Section atomic_snapshot.
 
   Lemma read_spec γ p :
     is_snapshot γ p -∗
-    <<< ∀∀ v : val, snapshot_content γ v >>>
+    <<{ ∀∀ v : val, snapshot_content γ v }>>
       read p @ ↑N
-    <<< snapshot_content γ v, RET v >>>.
+    <<{ snapshot_content γ v | RET v }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU".
     iDestruct "Hx" as (l1 ->) "#Hinv".
@@ -295,9 +295,9 @@ Section atomic_snapshot.
 
   Lemma read_with_spec γ p (l : loc) :
     is_snapshot γ p -∗
-    <<< ∀∀ v1 v2 : val, snapshot_content γ v1 ∗ l ↦ v2 >>>
+    <<{ ∀∀ v1 v2 : val, snapshot_content γ v1 ∗ l ↦ v2 }>>
        read_with_proph p #l @ ↑N
-    <<< snapshot_content γ v1 ∗ l ↦ v2, RET (v1, v2) >>>.
+    <<{ snapshot_content γ v1 ∗ l ↦ v2 | RET (v1, v2) }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH". wp_lam. wp_pures.
     (* ************ new prophecy ********** *)
diff --git a/theories/logatom/snapshot/spec.v b/theories/logatom/snapshot/spec.v
index 1f11f61d137b3ba5da321d4e0e4b941cec7745e7..6f8f64cda4b564aa15f4e2550d428a29b673b1c6 100644
--- a/theories/logatom/snapshot/spec.v
+++ b/theories/logatom/snapshot/spec.v
@@ -27,19 +27,19 @@ Record atomic_snapshot {Σ} `{!heapGS Σ} := AtomicSnapshot {
       {{{ True }}} new_snapshot v {{{ γ p, RET p; is_snapshot N γ p ∗ snapshot_content γ v }}};
     read_spec N γ p :
       is_snapshot N γ p -∗
-      <<< ∀∀ v : val, snapshot_content γ v  >>>
+      <<{ ∀∀ v : val, snapshot_content γ v  }>>
         read p @ ↑N
-      <<< snapshot_content γ v, RET v >>>;
+      <<{ snapshot_content γ v | RET v }>>;
     write_spec N γ (v: val) p :
       is_snapshot N γ p -∗
-      <<< ∀∀ w : val, snapshot_content γ w  >>>
+      <<{ ∀∀ w : val, snapshot_content γ w  }>>
         write p v @ ↑N
-      <<< snapshot_content γ v, RET #() >>>;
+      <<{ snapshot_content γ v | RET #() }>>;
     read_with_spec N γ p (l : loc) :
       is_snapshot N γ p -∗
-      <<< ∀∀ v w : val, snapshot_content γ v ∗ l ↦ w >>>
+      <<{ ∀∀ v w : val, snapshot_content γ v ∗ l ↦ w }>>
         read_with p #l @ ↑N
-      <<< snapshot_content γ v ∗ l ↦ w, RET (v, w) >>>;
+      <<{ snapshot_content γ v ∗ l ↦ w | RET (v, w) }>>;
 }.
 Global Arguments atomic_snapshot _ {_}.
 
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
index 44060156535845ce9d55c0856a2f868f1304f61a..5e2d9e3a0a44eece8a2434d29827c61d00fe3a68 100644
--- a/theories/logatom/treiber.v
+++ b/theories/logatom/treiber.v
@@ -83,9 +83,9 @@ Section proof.
   Qed.
 
   Lemma push_atomic_spec (s: loc) (x: val) :
-    ⊢ <<< ∀∀ (xs : list val), is_stack s xs >>>
+    ⊢ <<{ ∀∀ (xs : list val), is_stack s xs }>>
         push #s x @ ∅
-      <<< is_stack s (x::xs), RET #() >>>.
+      <<{ is_stack s (x::xs) | RET #() }>>.
   Proof.
     unfold is_stack.
     iIntros (Φ) "HP". iLöb as "IH". wp_rec.
@@ -110,11 +110,11 @@ Section proof.
   Qed.
 
   Lemma pop_atomic_spec (s: loc) :
-    ⊢ <<< ∀∀ (xs : list val), is_stack s xs >>>
+    ⊢ <<{ ∀∀ (xs : list val), is_stack s xs }>>
         pop #s @ ∅
-      <<< match xs with [] => is_stack s []
-                  | x::xs' => is_stack s xs' end,
-      RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
+      <<{ match xs with [] => is_stack s []
+                  | x::xs' => is_stack s xs' end
+        | RET match xs with [] => NONEV | x :: _ => SOMEV x end }>>.
   Proof.
     unfold is_stack.
     iIntros (Φ) "HP". iLöb as "IH". wp_rec.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index d67cd99abb6bdca7b4c5b9b1d332dae58900f87c..d383d96e58cc941acac7179024f7e64f30131f14 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -238,9 +238,9 @@ Qed.
     the possibility of accessing the precondition again, unlike with abort. *)
 Lemma push_stack_spec (ℓ : loc) (γ : gname) (v : val) :
   is_stack ℓ γ -∗
-  <<< ∀∀ (xs : list val), stack_cont γ xs >>>
+  <<{ ∀∀ (xs : list val), stack_cont γ xs }>>
     push_stack v #ℓ @ ↑N
-  <<< stack_cont γ (v :: xs) , RET #() >>>.
+  <<{ stack_cont γ (v :: xs)  | RET #() }>>.
 Proof.
   (* Introduce things into the Coq and Iris contexts, and use induction. *)
   iIntros "#HInv" (Φ) "AU". iLöb as "IH".
@@ -290,10 +290,10 @@ Qed.
     the postcondition also depends on the emptiness of the stack. *)
 Lemma pop_stack_spec (ℓ : loc) (γ : gname) :
   is_stack ℓ γ -∗
-  <<< ∀∀ (xs : list val), stack_cont γ xs >>>
+  <<{ ∀∀ (xs : list val), stack_cont γ xs }>>
     pop_stack #ℓ @ ↑N
-  <<< stack_cont γ (match xs with [] => [] | _::xs => xs end)
-    , RET (match xs with [] => NONEV | v::_ => SOMEV v end) >>>.
+  <<{ stack_cont γ (match xs with [] => [] | _::xs => xs end)
+    | RET (match xs with [] => NONEV | v::_ => SOMEV v end) }>>.
 Proof.
   (* As for [push_stack], we need to use induction and the focus on a load. *)
   iIntros "#HInv" (Φ) "AU". iLöb as "IH". wp_lam. wp_bind (! _)%E.