diff --git a/CHANGELOG.md b/CHANGELOG.md
index 71fffacb89076f44779fead315b2eb387fc63208..bc64412a43aa1bcbc5ce02a3a7a8fffd09634d72 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -118,6 +118,8 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
 * Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
 * Add `Plain` instance for `|==> P` when `P` is plain.
 * Rename `bupd_plain` → `bupd_elim`.
+* Change notation for atomic updates and atomic accessors to use `<{ ... }>`
+  instead of `<< ... >>`. This avoids a conflict with Autosubst.
 
 **Changes in `proofmode`:**
 
@@ -182,6 +184,15 @@ Coq 8.13, 8.14, and 8.15 are no longer supported.
 * Remove `frac_validI`. Instead, move to the pure context (with `%` in the proof
   mode or `uPred.discrete_valid` in manual proofs) and use `frac_valid`.
 
+**Changes in `program_logic`:**
+
+* Change the notation for logically atomic triples: we add support for specifying private (non-atomic) postconditions,
+  and we avoid a notation conflict with Autosubst. The new notation looks as follows:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | z, RET v, non_atomic_post x y z }>>`.
+  To keep the notation without private postcondition consistent, the way the return value is specified changes slightly
+  even when there is no private postcondition:
+  `<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | RET v }>>`.
+
 **Changes in `heap_lang`:**
 
 * Move operations and lemmas about locations into a module `Loc`.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 3ac2c2a0918645dd7293d00c7a81b540b2742df8..7874ea37a504c7cbd9a9e0a1927e237fe180e86b 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -96,9 +96,11 @@ Global Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
 Global Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
 
 (** Notation: Atomic updates *)
+(** We avoid '<<'/'>>' since those can also reasonably be infix operators
+(and in fact Autosubst uses the latter). *)
+Notation "'AU' '<{' ∃∃ x1 .. xn , α '}>' @ Eo , Ei '<{' ∀∀ y1 .. yn , β , 'COMM' Φ '}>'" :=
 (* The way to read the [tele_app foo] here is that they convert the n-ary
 function [foo] into a unary function taking a telescope as the argument. *)
-Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                  (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                  Eo Ei
@@ -111,9 +113,9 @@ Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , 
                         ) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<{'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<{' ∃∃ x1 .. xn , α '}>' @ Eo , Ei '<{' β , 'COMM' Φ '}>'" :=
   (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
                  (TB:=TeleO)
                  Eo Ei
@@ -122,9 +124,9 @@ Notation "'AU' '<<' ∃∃ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'
                  (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<{'  '[' ∃∃  x1  ..  xn ,  '/' α  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<{' α '}>' @ Eo , Ei '<{' ∀∀ y1 .. yn , β , 'COMM' Φ '}>'" :=
   (atomic_update (TA:=TeleO)
                  (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
                  Eo Ei
@@ -133,9 +135,9 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'
                  (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<{'  '[' α  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AU' '<{' α '}>' @ Eo , Ei '<{' β , 'COMM' Φ '}>'" :=
   (atomic_update (TA:=TeleO) (TB:=TeleO)
                  Eo Ei
                  (tele_app α%I)
@@ -143,10 +145,10 @@ Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
                  (tele_app $ tele_app Φ%I)
   )
   (at level 20, Eo, Ei, α, β, Φ at level 200,
-   format "'[hv   ' 'AU'  '<<'  '[' α  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv   ' 'AU'  '<{'  '[' α  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
 (** Notation: Atomic accessors *)
-Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<{' ∃∃ x1 .. xn , α , 'ABORT' P '}>' @ Eo , Ei '<{' ∀∀ y1 .. yn , β , 'COMM' Φ '}>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -160,9 +162,9 @@ Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀
                      ) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<{'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<{' ∃∃ x1 .. xn , α , 'ABORT' P '}>' @ Eo , Ei '<{' β , 'COMM' Φ '}>'" :=
   (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
               (TB:=TeleO)
               Eo Ei
@@ -172,9 +174,9 @@ Notation "'AACC' '<<' ∃∃ x1 .. xn , α , 'ABORT' P '>>' @ Eo , Ei '<<' β ,
               (tele_app $ λ x1, .. (λ xn, tele_app Φ%I) .. )
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<{'  '[' ∃∃  x1  ..  xn ,  '/' α ,  '/' ABORT  P  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<{' α , 'ABORT' P '}>' @ Eo , Ei '<{' ∀∀ y1 .. yn , β , 'COMM' Φ '}>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
               Eo Ei
@@ -184,9 +186,9 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' ∀∀ y1 .. yn , β ,
               (tele_app $ tele_app (λ y1, .. (λ yn, Φ%I) ..))
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
-   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<{'  '[' α ,  '/' ABORT  P  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' ∀∀  y1  ..  yn ,  '/' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
-Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+Notation "'AACC' '<{' α , 'ABORT' P '}>' @ Eo , Ei '<{' β , 'COMM' Φ '}>'" :=
   (atomic_acc (TA:=TeleO)
               (TB:=TeleO)
               Eo Ei
@@ -196,7 +198,7 @@ Notation "'AACC' '<<' α , 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
               (tele_app $ tele_app Φ%I)
   )
   (at level 20, Eo, Ei, α, P, β, Φ at level 200,
-   format "'[hv     ' 'AACC'  '<<'  '[' α ,  '/' ABORT  P  ']' '>>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<<'  '[' β ,  '/' COMM  Φ  ']' '>>' ']'") : bi_scope.
+   format "'[hv     ' 'AACC'  '<{'  '[' α ,  '/' ABORT  P  ']' '}>'  '/' @  '[' Eo ,  '/' Ei ']'  '/' '<{'  '[' β ,  '/' COMM  Φ  ']' '}>' ']'") : bi_scope.
 
 (** Lemmas about AU *)
 Section lemmas.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index f4f967d6031dd0a75c5dee408510b7f7cfa326cb..82ed2188b3e475080c4c5bcb763898dfb4a947a0 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -1,3 +1,45 @@
+(** This file declares notation for logically atomic Hoare triples, and some
+generic lemmas about them. To enable the definition of a shared theory applying
+to triples with any number of binders, the triples themselves are defined via telescopes, but as a user
+you need not be concerned with that. You can just use the following notation:
+
+  <<{ ∀∀ x, atomic_precondition }>>
+    code @ E
+  <<{ ∃∃ y, atomic_postcondition | z, RET return_value; private_postcondition }>>
+
+Here, [x] (which can be any number of binders, including 0) is bound in all of
+the atomic pre- and postcondition and the private (non-atomic) postcondition and
+the return value, [y] (which can be any number of binders, including 0) is bound
+in both postconditions and the return value, and [z] (which can be any number of
+binders, including 0) is bound in the return value and the private
+postcondition.
+
+Note that atomic triples are *not* implicitly persistent, unlike Texan triples.
+If you need a private (non-atomic) precondition, you can use a magic wand:
+
+  private_precondition -∗
+  <<{ ∀∀ x, atomic_precondition }>>
+    code @ E
+  <<{ ∃∃ y, atomic_postcondition
+    | z, RET return_value; private_postcondition }>>
+
+If you don't need a private postcondition, you can leave it away, e.g.:
+
+  <<{ ∀∀ x, atomic_precondition }>>
+    code @ E
+  <<{ ∃∃ y, atomic_postcondition | RET return_value }>>
+
+Note that due to combinatorial explosion and because Coq does not have a
+facility to declare such notation in a compositional way, not *all* variants of
+this notation exist: if you have binders before the [RET] (which is very
+uncommon), you must have a private postcondition (it can be [True]), and you
+must have [∀∀] and [∃∃] binders (they can be [_: ()]).
+
+For an example for how to prove and use logically atomic specifications, see
+[iris_heap_lang/lib/increment.v].
+
+*)
+
 From stdpp Require Import namespaces.
 From iris.bi Require Import telescopes.
 From iris.bi.lib Require Export atomic.
@@ -7,140 +49,269 @@ From iris.base_logic Require Import invariants.
 From iris.prelude Require Import options.
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
-example where we want it to be anything else. *)
-Definition atomic_wp `{!irisGS_gen hlc Λ Σ} {TA TB : tele}
+example where we want it to be anything else.
+
+For the non-atomic post-condition, we use an [option PROP], combined with a
+[-∗?]. This is to avoid introducing spurious [True -∗] into proofs that do not
+need a non-atomic post-condition (which is most of them). *)
+Definition atomic_wp `{!irisGS_gen hlc Λ Σ} {TA TB TP : tele}
   (e: expr Λ) (* expression *)
   (E : coPset) (* *implementation* mask *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
-  (f: TA → TB → val Λ) (* Turn the return data into the return value *)
+  (POST: TA → TB → TP → option (iProp Σ)) (* non-atomic post-condition *)
+  (f: TA → TB → TP → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
     ∀ (Φ : val Λ → iProp Σ),
             (* The (outer) user mask is what is left after the implementation
             opened its things. *)
-            atomic_update (⊤∖E) ∅ α β (λ.. x y, Φ (f x y)) -∗
+            atomic_update (⊤∖E) ∅ α β (λ.. x y, ∀.. z, POST x y z -∗? Φ (f x y z)) -∗
             WP e {{ Φ }}.
-(* Note: To add a private postcondition, use
-   atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
 
+(** We avoid '<<{'/'}>>' since those can also reasonably be infix operators
+(and in fact Autosubst uses the latter). *)
+Notation "'<<{' ∀∀ x1 .. xn , α '}>>' e @ E '<<{' ∃∃ y1 .. yn , β '|' z1 .. zn , 'RET' v ; POST '}>>'" :=
 (* The way to read the [tele_app foo] here is that they convert the n-ary
 function [foo] into a unary function taking a telescope as the argument. *)
-Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleS (λ z1, .. (TeleS (λ zn, TeleO)) .. ))
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn,
+                                   tele_app $ λ z1, .. (λ zn, Some POST%I) ..
+                                  ) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn,
+                                   tele_app $ λ z1, .. (λ zn, v%V) ..
+                                  ) ..
+                        ) .. )
+  )
+  (at level 20, E, β, α, v, POST at level 200, x1 binder, xn binder, y1 binder, yn binder, z1 binder, zn binder,
+   format "'[hv' '<<{'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' ∃∃  y1  ..  yn ,  '/' β  '|'  '/' z1  ..  zn ,  RET  v ;  '/' POST  ']' '}>>' ']'")
+  : bi_scope.
+
+(* There are overall 16 of possible variants of this notation:
+- with and without ∀∀ binders
+- with and without ∃∃ binders
+- with and without RET binders
+- with and without POST
+
+However we don't support the case where RET binders are present but anything
+else is missing. Below we declare the 8 notations that involve no RET binders.
+*)
+
+(* No RET binders *)
+Notation "'<<{' ∀∀ x1 .. xn , α '}>>' e @ E '<<{' ∃∃ y1 .. yn , β '|' 'RET' v ; POST '}>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
              e%E
              E
              (tele_app $ λ x1, .. (λ xn, α%I) ..)
              (tele_app $ λ x1, .. (λ xn,
-                         tele_app (λ y1, .. (λ yn, β%I) .. )
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app $ Some POST%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app $ v%V) ..
+                        ) .. )
+  )
+  (at level 20, E, β, α, v, POST at level 200, x1 binder, xn binder, y1 binder, yn binder,
+   format "'[hv' '<<{'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' ∃∃  y1  ..  yn ,  '/' β  '|'  '/' RET  v ;  '/' POST  ']' '}>>' ']'")
+  : bi_scope.
+
+(* No ∃∃ binders, no RET binders *)
+Notation "'<<{' ∀∀ x1 .. xn , α '}>>' e @ E '<<{' β '|' 'RET' v ; POST '}>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleO)
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ tele_app $ Some POST%I
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ tele_app $ v%V
+                        ) .. )
+  )
+  (at level 20, E, β, α, v, POST at level 200, x1 binder, xn binder,
+   format "'[hv' '<<{'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' β  '|'  '/' RET  v ;  '/' POST  ']' '}>>' ']'")
+  : bi_scope.
+
+(* No ∀∀ binders, no RET binders *)
+Notation "'<<{' α '}>>' e @ E '<<{' ∃∃ y1 .. yn , β '|' 'RET' v ; POST '}>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ α%I)
+             (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app $ Some POST%I) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app $ v%V) .. )
+  )
+  (at level 20, E, β, α, v, POST at level 200, y1 binder, yn binder,
+   format "'[hv' '<<{'  '[' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' ∃∃  y1  ..  yn ,  '/' β  '|'  '/' RET  v ;  '/' POST  ']' '}>>' ']'")
+  : bi_scope.
+
+(* No ∀∀ binders, no ∃∃ binders, no RET binders *)
+Notation "'<<{' α '}>>' e @ E '<<{' β '|' 'RET' v ; POST '}>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleO)
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ α%I)
+             (tele_app $ tele_app β%I)
+             (tele_app $ tele_app $ tele_app $ Some POST%I)
+             (tele_app $ tele_app $ tele_app $ v%V)
+  )
+  (at level 20, E, β, α, v, POST at level 200,
+   format "'[hv' '<<{'  '[' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' β  '|'  '/' RET  v ;  '/' POST  ']' '}>>' ']'")
+  : bi_scope.
+
+(* No RET binders, no POST *)
+Notation "'<<{' ∀∀ x1 .. xn , α '}>>' e @ E '<<{' ∃∃ y1 .. yn , β '|' 'RET' v '}>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app None) ..
                         ) .. )
              (tele_app $ λ x1, .. (λ xn,
-                         tele_app (λ y1, .. (λ yn, v%V) .. )
+                         tele_app $ λ y1, .. (λ yn, tele_app v%V) ..
                         ) .. )
   )
-  (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+  (at level 20, E, β, α, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
+   format "'[hv' '<<{'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' ∃∃  y1  ..  yn ,  '/' β  '|'  '/' RET  v  ']' '}>>' ']'")
   : bi_scope.
 
-Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
+(* No ∃∃ binders, no RET binders, no POST *)
+Notation "'<<{' ∀∀ x1 .. xn , α '}>>' e @ E '<<{' β '|' 'RET' v '}>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
+             (TP:=TeleO)
              e%E
              E
              (tele_app $ λ x1, .. (λ xn, α%I) ..)
              (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
-             (tele_app $ λ x1, .. (λ xn, tele_app v%V) .. )
+             (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app None) .. )
+             (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app v%V) .. )
   )
-  (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+  (at level 20, E, β, α, v at level 200, x1 binder, xn binder,
+   format "'[hv' '<<{'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' β  '|'  '/' RET  v  ']' '}>>' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
+(* No ∀∀ binders, no RET binders, no POST *)
+Notation "'<<{' α '}>>' e @ E '<<{' ∃∃ y1 .. yn , β '|' 'RET' v '}>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
              e%E
              E
              (tele_app α%I)
-             (tele_app $ tele_app (λ y1, .. (λ yn, β%I) .. ))
-             (tele_app $ tele_app (λ y1, .. (λ yn, v%V) .. ))
+             (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app None) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app v%V) .. )
   )
-  (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+  (at level 20, E, β, α, v at level 200, y1 binder, yn binder,
+   format "'[hv' '<<{'  '[' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' ∃∃  y1  ..  yn ,  '/' β  '|'  '/' RET  v  ']' '}>>' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
+(* No ∀∀ binders, no ∃∃ binders, no RET binders, no POST *)
+Notation "'<<{' α '}>>' e @ E '<<{' β '|' 'RET' v '}>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleO)
+             (TP:=TeleO)
              e%E
              E
              (tele_app α%I)
              (tele_app $ tele_app β%I)
-             (tele_app $ tele_app v%V)
+             (tele_app $ tele_app $ tele_app None)
+             (tele_app $ tele_app $ tele_app v%V)
   )
-  (at level 20, E, α, β, v at level 200,
-   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+  (at level 20, E, β, α, v at level 200,
+   format "'[hv' '<<{'  '[' α  ']' '}>>'  '/  ' e  @  E  '/' '<<{'  '[' β  '|'  '/' RET  v  ']' '}>>' ']'")
   : bi_scope.
 
 (** Theory *)
 Section lemmas.
-  Context `{!irisGS_gen hlc Λ Σ} {TA TB : tele}.
+  Context `{!irisGS_gen hlc Λ Σ} {TA TB TP : tele}.
   Notation iProp := (iProp Σ).
-  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
+  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (POST : TA → TB → TP → option iProp) (f : TA → TB → TP → val Λ).
 
   (* Atomic triples imply sequential triples. *)
-  Lemma atomic_wp_seq e E α β f :
-    atomic_wp e E α β f -∗
-    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Lemma atomic_wp_seq e E α β POST f :
+    atomic_wp e E α β POST f -∗
+    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros "Hwp" (Φ x) "Hα HΦ".
     iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-    rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
+    rewrite ->!tele_app_bind. iIntros (z) "Hpost HΦ". iApply ("HΦ" with "Hβ Hpost").
   Qed.
 
   (** This version matches the Texan triple, i.e., with a later in front of the
   [(∀.. y, β x y -∗ Φ (f x y))]. *)
-  Lemma atomic_wp_seq_step e E α β f :
+  Lemma atomic_wp_seq_step e E α β POST f :
     TCEq (to_val e) None →
-    atomic_wp e E α β f -∗
-    ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+    atomic_wp e E α β POST f -∗
+    ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
-    iApply (wp_step_fupd _ _ ⊤ _ (∀.. y : TB, β x y -∗ Φ (f x y))
+    iApply (wp_step_fupd _ _ ⊤ _ (∀.. y : TB, _)
       with "[$HΦ //]"); first done.
     iApply (atomic_wp_seq with "H Hα").
-    iIntros (y) "Hβ HΦ". by iApply "HΦ".
+    iIntros "%y Hβ %z Hpost HΦ". iApply ("HΦ" with "Hβ Hpost").
   Qed.
 
   (* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
-  Lemma atomic_seq_wp_atomic e E α β f `{!Atomic WeaklyAtomic e} :
-    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
-    atomic_wp e E α β f.
+  Lemma atomic_seq_wp_atomic e E α β POST f `{!Atomic WeaklyAtomic e} :
+    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e @ ∅ {{ Φ }}) -∗
+    atomic_wp e E α β POST f.
   Proof.
     iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
-    iApply ("Hwp" with "Hα"). iIntros (y) "Hβ".
+    iApply ("Hwp" with "Hα"). iIntros "%y Hβ %z Hpost".
     iMod ("Hclose" with "Hβ") as "HΦ".
-    rewrite ->!tele_app_bind. iApply "HΦ".
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
   Qed.
 
   (** Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
   Lemma persistent_seq_wp_atomic e E (α : [tele] → iProp) (β : [tele] → TB → iProp)
-        (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
-    (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
-    atomic_wp e E α β f.
+      (POST : [tele] → TB → TP → option iProp) (f : [tele] → TB → TP → val Λ)
+      {HP : Persistent (α [tele_arg])} :
+    (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ ∀.. z, POST [tele_arg] y z -∗? Φ (f [tele_arg] y z)) -∗ WP e {{ Φ }}) -∗
+    atomic_wp e E α β POST f.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
-    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
+    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!> %y Hβ %z Hpost".
     iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-    rewrite ->!tele_app_bind. done.
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
   Qed.
 
-  Lemma atomic_wp_mask_weaken e E1 E2 α β f :
-    E1 ⊆ E2 → atomic_wp e E1 α β f -∗ atomic_wp e E2 α β f.
+  Lemma atomic_wp_mask_weaken e E1 E2 α β POST f :
+    E1 ⊆ E2 → atomic_wp e E1 α β POST f -∗ atomic_wp e E2 α β POST f.
   Proof.
     iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
     iApply atomic_update_mask_weaken; last done. set_solver.
@@ -148,10 +319,10 @@ Section lemmas.
 
   (** We can open invariants around atomic triples.
       (Just for demonstration purposes; we always use [iInv] in proofs.) *)
-  Lemma atomic_wp_inv e E α β f N I :
+  Lemma atomic_wp_inv e E α β POST f N I :
     ↑N ⊆ E →
-    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
-    inv N I -∗ atomic_wp e E α β f.
+    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) POST f -∗
+    inv N I -∗ atomic_wp e E α β POST f.
   Proof.
     intros ?. iIntros "Hwp #Hinv" (Φ) "AU". iApply "Hwp". iAuIntro.
     iInv N as "HI". iApply (aacc_aupd with "AU"); first solve_ndisj.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index b356f550a02a286628da3b12dbac3a0046fa77c6..2c4532bf7c366fdb9bf4348e2fd2b21ad74cae87 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -56,10 +56,10 @@ Class atomic_heap := AtomicHeap {
   free_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (v : val) :
     {{{ mapsto (H:=H) l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) :
-    ⊢ <<< ∀∀ (v : val) q, mapsto (H:=H) l q v >>> load #l @ ∅ <<< mapsto (H:=H) l q v, RET v >>>;
+    ⊢ <<{ ∀∀ (v : val) q, mapsto (H:=H) l q v }>> load #l @ ∅ <<{ mapsto (H:=H) l q v | RET v }>>;
   store_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w : val) :
-    ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> store #l w @ ∅
-      <<< mapsto (H:=H) l (DfracOwn 1) w, RET #() >>>;
+    ⊢ <<{ ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v }>> store #l w @ ∅
+      <<{ mapsto (H:=H) l (DfracOwn 1) w | RET #() }>>;
   (* 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
@@ -68,10 +68,10 @@ Class atomic_heap := AtomicHeap {
   [destruct (decide (a = b))] and it will simplify in both places. *)
   cmpxchg_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
-      <<< if decide (v = w1)
-          then mapsto (H:=H) l (DfracOwn 1) w2 else mapsto (H:=H) l (DfracOwn 1) v,
-        RET (v, #if decide (v = w1) then true else false) >>>;
+    ⊢ <<{ ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v }>> cmpxchg #l w1 w2 @ ∅
+      <<{ if decide (v = w1)
+          then mapsto (H:=H) l (DfracOwn 1) w2 else mapsto (H:=H) l (DfracOwn 1) v
+        | RET (v, #if decide (v = w1) then true else false) }>>;
 }.
 
 Global Arguments alloc : simpl never.
@@ -112,11 +112,11 @@ Section derived.
 
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>>
+    ⊢ <<{ ∀∀ v, mapsto l (DfracOwn 1) v }>>
       CAS #l w1 w2 @ ∅
-    <<< if decide (v = w1)
-        then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
-      RET #if decide (v = w1) then true else false >>>.
+    <<{ if decide (v = w1)
+        then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v
+      | RET #if decide (v = w1) then true else false }>>.
   Proof.
     iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
     iApply (aacc_aupd_commit with "AU"); first done.
@@ -125,9 +125,9 @@ Section derived.
   Qed.
 
   Lemma faa_spec (l : loc) (i2 : Z) :
-    ⊢ <<< ∀∀ i1 : Z, mapsto l (DfracOwn 1) #i1 >>>
+    ⊢ <<{ ∀∀ i1 : Z, mapsto l (DfracOwn 1) #i1 }>>
       FAA #l #i2 @ ∅
-    <<< mapsto l (DfracOwn 1) #(i1 + i2), RET #i1 >>>.
+    <<{ mapsto l (DfracOwn 1) #(i1 + i2) | RET #i1 }>>.
   Proof.
     iIntros (Φ) "AU". rewrite /faa_atomic. iLöb as "IH".
     wp_pures. awp_apply load_spec.
@@ -174,8 +174,8 @@ Section proof.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    ⊢ <<< ∀∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
-    <<< l ↦{q} v, RET v >>>.
+    ⊢ <<{ ∀∀ (v : val) q, l ↦{q} v }>> primitive_load #l @ ∅
+      <<{ l ↦{q} v | RET v }>>.
   Proof.
     iIntros (Φ) "AU". wp_lam.
     iMod "AU" as (v q) "[H↦ [_ Hclose]]".
@@ -183,8 +183,8 @@ Section proof.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀∀ v, l ↦ v >>> primitive_store #l w @ ∅
-    <<< l ↦ w, RET #() >>>.
+    ⊢ <<{ ∀∀ v, l ↦ v }>> primitive_store #l w @ ∅
+      <<{ l ↦ w | RET #() }>>.
   Proof.
     iIntros (Φ) "AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
@@ -193,10 +193,10 @@ Section proof.
 
   Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀∀ (v : val), l ↦ v >>>
+    ⊢ <<{ ∀∀ (v : val), l ↦ v }>>
       primitive_cmpxchg #l w1 w2 @ ∅
-    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
-        RET (v, #if decide (v = w1) then true else false) >>>.
+    <<{ if decide (v = w1) then l ↦ w2 else l ↦ v
+      | RET (v, #if decide (v = w1) then true else false) }>>.
   Proof.
     iIntros (? Φ) "AU". wp_lam. wp_pures.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index b8c82febf7213bdde1d0326729a8a85ea8ba1e25..548609124cf1607e82c9e15706864181d2d81ff1 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
          else "incr" "l".
 
   Lemma incr_phy_spec (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr_phy #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -54,7 +54,7 @@ Section increment.
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -93,7 +93,7 @@ Section increment.
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)
   Lemma incr_spec (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -127,9 +127,10 @@ Section increment.
      connective that works on [option Qp] (the type of 1-q). *)
   Lemma weak_incr_spec (l: loc) (v : Z) :
     l ↦{#1/2} #v -∗
-    <<< ∀∀ (v' : Z), l ↦{#1/2} #v' >>>
+    <<{ ∀∀ (v' : Z), l ↦{#1/2} #v' }>>
       weak_incr #l @ ∅
-    <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
+    <<{ ⌜v = v'⌝ ∗ l ↦ #(v + 1)
+      | RET #v }>>.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl") as "Hl".
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 859fea3d5c193275f0e228cd08050cff813a9fb6..61ed4eb431156d579898518e05aac8e0d5ed7347 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -71,9 +71,9 @@ Section tada.
 
   Lemma acquire_tada_spec γ lk :
     tada_is_lock γ lk -∗
-    <<< ∀∀ s, tada_lock_state γ s >>>
+    <<{ ∀∀ s, tada_lock_state γ s }>>
       acquire lk @ ∅
-    <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked, RET #() >>>.
+    <<{ ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked | RET #() }>>.
   Proof.
     iIntros "#Hislock %Φ AU". iApply wp_fupd.
     wp_apply (acquire_spec with "Hislock") as "[Hlocked Hvar1]".
@@ -86,9 +86,9 @@ Section tada.
 
   Lemma release_tada_spec γ lk :
     tada_is_lock γ lk -∗
-    <<< tada_lock_state γ Locked >>>
+    <<{ tada_lock_state γ Locked }>>
       release lk @ ∅
-    <<< 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/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 7c048fcf5093e6a0620da164f730f229668ed666..4d72ae4faec7bcb0a48eba05296bcc8674fd06ac 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -727,7 +727,8 @@ premise. The second one additionaly does some framing: it gets rid of [Hs] from
 the context, reducing clutter. You get them all back in the continuation of the
 atomic operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
+  (* [pm_prettify] is needed to clean up telescopes. *)
+  wp_apply_core lem ltac:(fun H => iApplyHyp H; pm_prettify) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   (* Convert "list of hypothesis" into specialization pattern. *)
@@ -736,7 +737,8 @@ Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   wp_apply_core lem
     ltac:(fun H =>
       iApply (wp_frame_wand with
-        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
+        [SGoal $ SpecGoal GSpatial false [] Hs false]);
+         [iAccu|iApplyHyp H; pm_prettify])
     ltac:(fun cont => fail);
   last iAuIntro.
 
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 90a359e12dfccdd617576282f4644185eed71eef..7a3df20814a70a324e3be8d1eefb3b07636436c8 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,23 @@
+"test_awp_apply"
+     : string
+1 goal
+  
+  H : atomic_heap
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  atomic_heapGS0 : atomic_heapGS Σ
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "HQ" : Q
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC <{ ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT Q ∗ l ↦ v }>
+       @ ⊤ ∖ ∅, ∅
+       <{ l ↦{q} v0, COMM Q }>
+"test_awp_apply_without"
+     : string
 1 goal
   
   H : atomic_heap
@@ -10,9 +30,9 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  atomic_acc (⊤ ∖ ∅) ∅ (tele_app (λ (v0 : val) (q : dfrac), l ↦{q} v0))
-    (l ↦ v) (tele_app (λ (v0 : val) (q : dfrac), tele_app (l ↦{q} v0)))
-    (λ.. (_ : [tele (_ : val) (_ : dfrac)]) (_ : [tele]), Q -∗ Q)
+  AACC <{ ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v }>
+       @ ⊤ ∖ ∅, ∅
+       <{ l ↦{q} v0, COMM Q -∗ Q }>
 "printing"
      : string
 1 goal
@@ -21,7 +41,7 @@
   heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
-  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< ∃∃ y : val, P y, RET #() >>>
+  ⊢ <<{ ∀∀ x : val, P x }>> code @ ∅ <<{ ∃∃ y : val, P y | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -29,7 +49,7 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∃∃ x : val, P x >> @ ⊤, ∅ << ∀∀ y : val, P y, COMM Φ #() >>
+  "AU" : AU <{ ∃∃ x : val, P x }> @ ⊤, ∅ <{ ∀∀ y : val, P y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -39,12 +59,12 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∃∃ x : val, P x,
-              ABORT AU << ∃∃ x : val, P x >>
+  _ : AACC <{ ∃∃ x : val, P x,
+              ABORT AU <{ ∃∃ x : val, P x }>
                        @ ⊤, ∅
-                       << ∀∀ y : val, P y, COMM Φ #() >> >>
+                       <{ ∀∀ y : val, P y, COMM Φ #() }> }>
            @ ⊤, ∅
-           << ∀∀ y : val, P y, COMM Φ #() >>
+           <{ ∀∀ y : val, P y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -53,7 +73,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
+  ⊢ <<{ ∀∀ x : val, l ↦ x }>> code @ ∅ <<{ l ↦ x | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -61,7 +81,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∃∃ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
+  "AU" : AU <{ ∃∃ x : val, l ↦ x }> @ ⊤ ∖ ∅, ∅ <{ l ↦ x, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -71,12 +91,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << ∃∃ x : val, l ↦ x,
-              ABORT AU << ∃∃ x : val, l ↦ x >>
+  _ : AACC <{ ∃∃ x : val, l ↦ x,
+              ABORT AU <{ ∃∃ x : val, l ↦ x }>
                        @ ⊤ ∖ ∅, ∅
-                       << l ↦ x, COMM Φ #() >> >>
+                       <{ l ↦ x, COMM Φ #() }> }>
            @ ⊤ ∖ ∅, ∅
-           << l ↦ x, COMM Φ #() >>
+           <{ l ↦ x, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -85,7 +105,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ ∃∃ y : val, l ↦ y | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -93,7 +113,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∀∀ y : val, l ↦ y, COMM Φ #() >>
+  "AU" : AU <{ l ↦ #() }> @ ⊤ ∖ ∅, ∅ <{ ∀∀ y : val, l ↦ y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -103,12 +123,12 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #(),
-              ABORT AU << l ↦ #() >>
+  _ : AACC <{ l ↦ #(),
+              ABORT AU <{ l ↦ #() }>
                        @ ⊤ ∖ ∅, ∅
-                       << ∀∀ y : val, l ↦ y, COMM Φ #() >> >>
+                       <{ ∀∀ y : val, l ↦ y, COMM Φ #() }> }>
            @ ⊤ ∖ ∅, ∅
-           << ∀∀ y : val, l ↦ y, COMM Φ #() >>
+           <{ ∀∀ y : val, l ↦ y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -117,7 +137,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>
+  ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ l ↦ #() | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -125,7 +145,7 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
+  "AU" : AU <{ l ↦ #() }> @ ⊤ ∖ ∅, ∅ <{ l ↦ #(), COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -135,10 +155,10 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AACC << l ↦ #(),
-              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
+  _ : AACC <{ l ↦ #(),
+              ABORT AU <{ l ↦ #() }> @ ⊤ ∖ ∅, ∅ <{ l ↦ #(), COMM Φ #() }> }>
            @ ⊤ ∖ ∅, ∅
-           << l ↦ #(), COMM Φ #() >>
+           <{ l ↦ #(), COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 "Now come the long pre/post tests"
@@ -149,9 +169,9 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x >>>
+  ⊢ <<{ ∀∀ x : val, l ↦ x ∗ l ↦ x }>>
       code @ ∅
-    <<< ∃ y : val, l ↦ y, RET #() >>>
+    <<{ ∃ y : val, l ↦ y | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -159,9 +179,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x >>
+  "AU" : AU <{ ∃∃ x : val, l ↦ x ∗ l ↦ x }>
             @ ⊤ ∖ ∅, ∅
-            << ∃ y : val, l ↦ y, COMM Φ #() >>
+            <{ ∃ y : val, l ↦ y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -170,9 +190,9 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<{ ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>>
       code @ ∅
-    <<< ∃∃ y : val, l ↦ y, RET #() >>>
+    <<{ ∃∃ y : val, l ↦ y | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -180,9 +200,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU <{ ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>
             @ ⊤ ∖ ∅, ∅
-            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
+            <{ ∀∀ y : val, l ↦ y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -191,10 +211,10 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<{ ∀∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>>
       code @ ∅
-    <<< ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-        RET #() >>>
+    <<{ ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+        l ↦ xx ∗ l ↦ xx | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -202,10 +222,10 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : AU << ∃∃ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+  _ : AU <{ ∃∃ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>
          @ ⊤ ∖ ∅, ∅
-         << ∀∀ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
-            l ↦ xx, COMM Φ #() >>
+         <{ ∀∀ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+            l ↦ xx ∗ l ↦ xx, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -214,9 +234,9 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<{ ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>>
       code @ ∅
-    <<< l ↦ x, RET #() >>>
+    <<{ l ↦ x | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -224,9 +244,9 @@
   l : loc
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU <{ ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>
             @ ⊤ ∖ ∅, ∅
-            << l ↦ x, COMM Φ #() >>
+            <{ l ↦ x, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -236,9 +256,9 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>>
       code @ ∅
-    <<< ∃∃ y : val, l ↦ y, RET #() >>>
+    <<{ ∃∃ y : val, l ↦ y | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -247,9 +267,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU <{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>
             @ ⊤ ∖ ∅, ∅
-            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
+            <{ ∀∀ y : val, l ↦ y, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -259,9 +279,9 @@
   l : loc
   x : val
   ============================
-  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+  ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>>
       code @ ∅
-    <<< l ↦ #(), RET #() >>>
+    <<{ l ↦ #() | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -270,9 +290,9 @@
   x : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+  "AU" : AU <{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>
             @ ⊤ ∖ ∅, ∅
-            << l ↦ #(), COMM Φ #() >>
+            <{ l ↦ #(), COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -282,9 +302,9 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>>
       code @ ∅
-    <<< l ↦ yyyy, RET #() >>>
+    <<{ l ↦ yyyy | RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -293,9 +313,9 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+  "AU" : AU <{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>
             @ ⊤ ∖ ∅, ∅
-            << l ↦ yyyy, COMM Φ #() >>
+            <{ l ↦ yyyy, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -305,10 +325,10 @@
   l : loc
   xx, yyyy : val
   ============================
-  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+  ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>>
       code @ ∅
-    <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-        RET #() >>>
+    <<{ l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx |
+        RET #() }>>
 1 goal
   
   Σ : gFunctors
@@ -317,12 +337,49 @@
   xx, yyyy : val
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+  "AU" : AU <{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>
             @ ⊤ ∖ ∅, ∅
-            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
-               l ↦ xx, COMM Φ #() >>
+            <{ l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+               l ↦ xx, COMM Φ #() }>
   --------------------------------------∗
   WP code {{ v, Φ v }}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<{ ∀∀ x : val, P x }>>
+      code @ ∅
+    <<{ ∃∃ y : val, P y | z : val, RET z; P z }>>
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<{ ∀∀ x : val, P x }>> code @ ∅ <<{ ∃∃ y : val, P y | RET y; P y }>>
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<{ ∀∀ x : val, P x }>> code @ ∅ <<{ P x | RET x; P x }>>
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<{ P #() }>> code @ ∅ <<{ ∃∃ y : val, P y | RET y; P y }>>
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : iProp Σ
+  ============================
+  ⊢ <<{ P }>> code @ ∅ <<{ P | RET #42; P }>>
 "Prettification"
      : string
 1 goal
@@ -334,9 +391,9 @@
   ============================
   "AU" : ∃ x : val, P x ∗
            (P x ={∅,⊤}=∗
-            AU << ∃∃ x0 : val, P x0 >>
+            AU <{ ∃∃ x0 : val, P x0 }>
                @ ⊤ ∖ ∅, ∅
-               << ∀∀ y : val, P y, COMM Φ #() >>)
+               <{ ∀∀ y : val, P y, COMM Φ #() }>)
            ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
diff --git a/tests/atomic.v b/tests/atomic.v
index 32b5595bca4177690914c8c607b8ce369aac7615..e205b20c7a0315026d22168680df58dd22b21fc8 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -25,7 +25,15 @@ Section tests.
   Context `{!atomic_heap, !heapGS Σ, !atomic_heapGS Σ}.
   Import atomic_heap.notation.
 
-  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Check "test_awp_apply".
+  Lemma test_awp_apply (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec. Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+
+  Check "test_awp_apply_without".
   Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
     Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
   Proof.
@@ -34,36 +42,37 @@ Section tests.
   Qed.
 End tests.
 
-(* Test if AWP and the AU obtained from AWP print. *)
+(* Test if AWP and the AU obtained from AWP print (and also tests that all the AWP variants parse and type-check). *)
 Check "printing".
 Section printing.
   Context `{!heapGS Σ}.
 
   Definition code : expr := #().
 
+  (* Without private postcondition or RET binders *)
   Lemma print_both_quant (P : val → iProp Σ) :
-    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y, RET #() >>>.
+    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". rewrite difference_empty_L. Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_first_quant l :
-    ⊢ <<< ∀∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<{ ∀∀ x, l ↦ x }>> code @ ∅ <<{ l ↦ x | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_second_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_no_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>.
+    ⊢ <<{ l ↦ #() }>> code @ ∅ <<{ l ↦ #() | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
@@ -72,59 +81,83 @@ Section printing.
   Check "Now come the long pre/post tests".
 
   Lemma print_both_quant_long l :
-    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃ y, l ↦ y | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpre l :
-    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpost l :
-    ⊢ <<< ∀∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< ∃∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+    ⊢ <<{ ∀∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ ∃∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "?". Show.
   Abort.
 
   Lemma print_first_quant_long l :
-    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<{ ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ l ↦ x | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_second_quant_long l x :
-    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ ∃∃ y, l ↦ y | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_long l x :
-    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ #(), RET #() >>>.
+    ⊢ <<{ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x }>> code @ ∅ <<{ l ↦ #() | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpre l xx yyyy :
-    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< l ↦ yyyy, RET #() >>>.
+    ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ l ↦ yyyy | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpost l xx yyyy :
-    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+    ⊢ <<{ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx }>> code @ ∅ <<{ l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx | RET #() }>>.
   Proof.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
+  (* With private postcondition.
+  (Makes no big difference for the AU so we only print the initial triple here.) *)
+  Lemma print_all (P : val → iProp Σ) :
+    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | z, RET z; P z }>>.
+  Proof. Show. Abort.
+
+  Lemma print_no_ret (P : val → iProp Σ) :
+    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ ∃∃ y, P y | RET y; P y }>>.
+  Proof. Show. Abort.
+
+  Lemma print_no_ex_ret (P : val → iProp Σ) :
+    ⊢ <<{ ∀∀ x, P x }>> code @ ∅ <<{ P x | RET x; P x }>>.
+  Proof. Show. Abort.
+
+  Lemma print_no_all_ret (P : val → iProp Σ) :
+    ⊢ <<{ P #() }>> code @ ∅ <<{ ∃∃ y, P y | RET y; P y }>>.
+  Proof. Show. Abort.
+
+  Lemma print_no_all_ex_ret (P : iProp Σ) :
+    ⊢ <<{ P }>> code @ ∅ <<{ P | RET #42; P }>>.
+  Proof. Show. Abort.
+
+  (* misc *)
   Check "Prettification".
 
   Lemma iMod_prettify (P : val → iProp Σ) :
-    ⊢ <<< ∀∀ x, P x >>> !#0 @ ∅ <<< ∃∃ y, P y, RET #() >>>.
+    ⊢ <<{ ∀∀ x, P x }>> !#0 @ ∅ <<{ ∃∃ y, P y | RET #() }>>.
   Proof.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
 
+
 End printing.