diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d9d81aeb939ab528211dc733ab63e93d8aa3eebf..e0929c2987b5fa0c8723c7d836a272a53d6a86d6 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-09-07.0.7adc00e0") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-09-14.0.013913bf") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 4cdbd4c3d43830c3240011edf8a0b30cf02042cb..af6184c4f1d4ff425a9e83e08a2987d07311e825 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -695,7 +695,7 @@ Section arc.
   Lemma strong_count_spec γi γs γw γsw l t v (P : vProp) tid :
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
     {{{ GPS_SWReader l t () v γs ∗ P }}}
-      strong_count [ #l] in tid
+      strong_count [ #l] @ tid; ⊤
     {{{ (c : Z), RET #c; P ∗ ⌜0 < c⌝ }}}.
   Proof.
     iIntros "#INV #Hacc !# * [#RR HP] HΦ". iLöb as "IH". wp_rec.
@@ -748,7 +748,7 @@ Section arc.
     strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
     GPS_SWReader (l >> 1) t () v γw -∗
     {{{ P }}}
-      weak_count [ #l] in tid
+      weak_count [ #l] @ tid; ⊤
     {{{ (c : Z), RET #c; P ∗ ⌜-1 ≤ c⌝ }}}.
   Proof.
     iIntros "#INV #Hacc #RR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -808,7 +808,7 @@ Section arc.
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
     (∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
     GPS_SWReader l t () v γs -∗
-    {{{ P }}} clone_arc [ #l] in tid
+    {{{ P }}} clone_arc [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ strong_arc t' q' l γi γs γw γsw ∗ P1 q' }}}.
   Proof.
     iIntros "#INV #Hacc #WR #RR !# * HP HΦ". iLöb as "IH". wp_rec.
@@ -1031,7 +1031,7 @@ Section arc.
   Lemma downgrade_spec γi γs γw γsw l t v ts (P : vProp) tid:
     is_arc P1 P2 N γi γs γw γsw l -∗ strong_arc_acc l ts γi γs γw γsw P (⊤ ∖ ↑N) -∗
     GPS_SWReader (l >> 1) t () v γw -∗
-    {{{ P }}} downgrade [ #l] in tid
+    {{{ P }}} downgrade [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
   Proof.
     iIntros "#INV #Hacc #WR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1201,7 +1201,7 @@ Section arc.
     is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l t γi γs γw γsw P (⊤ ∖ ↑N) -∗
     (∃ t' v', GPS_SWReader l t' () v' γs) -∗
     GPS_SWReader (l >> 1) t () v γw -∗
-    {{{ P }}} clone_weak [ #l] in tid
+    {{{ P }}} clone_weak [ #l] @ tid; ⊤
     {{{ t' q', RET #☠; P ∗ weak_arc t' q' l γi γs γw γsw }}}.
   Proof.
     iIntros "#INV #Hacc #SR #WR !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1388,7 +1388,7 @@ Section arc.
     is_arc P1 P2 N γi γs γw γsw l -∗ weak_arc_acc l tw γi γs γw γsw P (⊤ ∖ ↑N) -∗
     (∃ t' v', GPS_SWReader (l >> 1) t' () v' γw) -∗
     GPS_SWReader l t () v γs -∗
-    {{{ P }}} upgrade [ #l] in tid
+    {{{ P }}} upgrade [ #l] @ tid; ⊤
     {{{ (b : bool) q, RET #b;
         P ∗ if b then ∃ ts, strong_arc ts q l γi γs γw γsw ∗ P1 q else True }}}.
   Proof.
@@ -1553,7 +1553,7 @@ Section arc.
 
   Lemma drop_weak_spec γi γs γw γsw l q tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
-    {{{ (∃ tw, weak_arc tw q l γi γs γw γsw) }}} drop_weak [ #l] in tid
+    {{{ (∃ tw, weak_arc tw q l γi γs γw γsw) }}} drop_weak [ #l] @ tid; ⊤
     {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l >> 1) ↦ #0 else True }}}.
   Proof.
     iIntros (?) "#INV !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -1811,7 +1811,7 @@ Section arc.
 
   Lemma drop_fake_spec γi γs γw γsw l tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
-    {{{ fake_arc l γi γs γw γsw ∗ P2 }}} drop_weak [ #l] in tid
+    {{{ fake_arc l γi γs γw γsw ∗ P2 }}} drop_weak [ #l] @ tid; ⊤
     {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l >> 1) ↦ #0 else True }}}.
   Proof.
     iIntros (?) "#INV !# * [HP HP2] HΦ". iLöb as "IH". wp_rec. wp_op.
@@ -2031,7 +2031,7 @@ Section arc.
   Lemma drop_arc_spec {HPn: HP2} γi γs γw γsw l q tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
     {{{ (∃ ts, strong_arc ts q l γi γs γw γsw) ∗ P1 q }}}
-      drop_arc [ #l] in tid
+      drop_arc [ #l] @ tid; ⊤
     {{{ (b : bool), RET #b ;
         if b then P1 1 ∗ fake_arc l γi γs γw γsw else True }}}.
   Proof.
@@ -2252,7 +2252,7 @@ Section arc.
 
   Lemma try_unwrap_spec {HPn: HP2} γi γs γw γsw l q tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
-    {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}} try_unwrap [ #l] in tid
+    {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}} try_unwrap [ #l] @ tid; ⊤
     {{{ (b : bool), RET #b ;
         if b then P1 1 ∗ fake_arc l γi γs γw γsw
         else (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}.
@@ -2380,7 +2380,7 @@ Section arc.
   Lemma is_unique_spec {HPn: HP2} γi γs γw γsw l q tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
     {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}
-      is_unique [ #l] in tid
+      is_unique [ #l] @ tid; ⊤
     {{{ (b : bool), RET #b ;
         if b then l ↦ #1 ∗ (l >> 1) ↦ #1 ∗ P1 1
         else (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}.
@@ -2605,7 +2605,7 @@ Section arc.
   Lemma try_unwrap_full_spec {HPn : HP2} γi γs γw γsw l q tid :
     histN ## N → is_arc P1 P2 N γi γs γw γsw l -∗
     {{{ (∃ t, strong_arc t q l γi γs γw γsw) ∗ P1 q }}}
-      try_unwrap_full [ #l] in tid
+      try_unwrap_full [ #l] @ tid; ⊤
     {{{ (x : fin 3), RET #x ;
         match x : nat with
         (* No other reference : we get everything. *)
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index a4f987f3a1a29e43641a56aaa63bb6c0adac2b3d..f6d611875027432a3f7f23a9724535c155bf92e3 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -111,7 +111,7 @@ Section proof.
   Lemma try_acquire_spec N l γ κ R q tid E
     (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
     ⎡ lft_ctx ⎤ -∗
-    {{{ lock_proto N l γ κ R ∗ (q).[κ] }}} try_acquire [ #l ] in tid @ E
+    {{{ lock_proto N l γ κ R ∗ (q).[κ] }}} try_acquire [ #l ] @ tid; E
     {{{ b, RET #b; (if b is true then R else True) ∗ (q).[κ] }}}.
   Proof.
     iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". wp_rec.
@@ -144,7 +144,7 @@ Section proof.
     (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
     ⎡ lft_ctx ⎤ -∗
     {{{ lock_proto N l γ κ R ∗ (q).[κ] }}}
-      acquire [ #l ] in tid @ E
+      acquire [ #l ] @ tid; E
     {{{ RET #☠; R ∗ (q).[κ] }}}.
   Proof.
     iIntros "#LFT !#" (Φ) "[#Hproto Htok] HΦ". iLöb as "IH". wp_rec.
@@ -158,7 +158,7 @@ Section proof.
     (DISJ: histN ## N) (SUB1: ↑N ⊆ E) (SUB2 :↑lftN ⊆ E) (SUB3: ↑histN ⊆ E) :
     ⎡ lft_ctx ⎤ -∗
     {{{ R ∗ lock_proto N l γ κ R ∗ (q).[κ] }}}
-      release [ #l ] in tid @ E
+      release [ #l ] @ tid; E
     {{{ RET #☠; (q).[κ] }}}.
   Proof.
     iIntros "#LFT !#" (Φ) "(HR & #Hproto & Htok) HΦ". wp_let.
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index aa3f254f47c1ba7a525f4deb551f92244b488f55..9920e71bffdc3afe8266c445f708b226adc0d3ee 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -22,7 +22,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
 Lemma wp_memcpy `{!noprolG Σ} tid E l1 l2 vl1 vl2 q (n : Z):
   ↑histN ⊆ E → Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
-    #l1 <-{n} !#l2 in tid @ E
+    #l1 <-{n} !#l2 @ tid; E
   {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index a5e4797c0844e56dcc745273e11ef8ce96a7b870..4c98f13b1e58ba11b5ed48e34912dac24b9acc30 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -86,8 +86,8 @@ Proof. solve_proper. Qed.
 (** The main proofs. *)
 Lemma spawn_spec Ψ e (f : val) tid :
   IntoVal e f →
-  {{{ ∀ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] in tid' {{ _, True }} }}}
-    spawn [e] in tid
+  {{{ ∀ γc γe c tid', finish_handle γc γe c Ψ -∗ WP f [ #c] @ tid'; ⊤ {{ _, True }} }}}
+    spawn [e] @ tid; ⊤
   {{{ γc γe c, RET #c; join_handle γc γe c Ψ }}}.
 Proof.
   iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=.
@@ -107,7 +107,7 @@ Qed.
 Lemma finish_spec Ψ c v γc γe tid
   (DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
   {{{ finish_handle γc γe c Ψ ∗ Ψ v }}}
-    finish [ #c; v] in tid
+    finish [ #c; v] @ tid; ⊤
   {{{ RET #☠; True }}}.
 Proof.
   iIntros (Φ) "[Hfin HΨ] HΦ".
@@ -127,7 +127,7 @@ Qed.
 
 Lemma join_spec Ψ c γc γe tid
   (DISJ1: (↑histN) ## (↑N : coPset)) (DISJ2: (↑escrowN) ## (↑N : coPset)) :
-  {{{ join_handle γc γe c Ψ }}} join [ #c] in tid {{{ v, RET v; Ψ v }}}.
+  {{{ join_handle γc γe c Ψ }}} join [ #c] @ tid; ⊤ {{{ v, RET v; Ψ v }}}.
 Proof.
   iIntros (Φ) "H HΦ".
   iDestruct "H" as (γi Ψ' t) "(R & (H† & He) & Hj & #HΨ')".
diff --git a/theories/lang/swap.v b/theories/lang/swap.v
index 30a59564890e465ca7f1390c895fd7f8d7932c84..abef3ec3391e4091f2400511fa24afabc7dbac34 100644
--- a/theories/lang/swap.v
+++ b/theories/lang/swap.v
@@ -13,7 +13,7 @@ Definition swap : val :=
 Lemma wp_swap `{!noprolG Σ} tid E l1 l2 vl1 vl2 (n : Z):
   ↑histN ⊆ E →  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
-    swap [ #l1; #l2; #n] in tid @ E
+    swap [ #l1; #l2; #n] @ tid; E
   {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index 0581f1c698276b8fcb5ba03994033cd0c3511dec..fc832ef3492ccba6863d88af9be9283a0d54990b 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -58,7 +58,7 @@ Lemma GPS_aSP_Read IP IPC l κ q R (o: memOrder) t s v γ tid E
                       IP true l γ t' s' v' ∗ R t' s' v') ∧
                   (IPC l γ t' s' v' ={E ∖ ↑N}=∗
                       IPC l γ t' s' v' ∗ R t' s' v'))) }}}
-    Read o #l in tid @ E
+    Read o #l @ tid; E
   {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝
       ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ ∗ (q).[κ]
       ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
@@ -80,7 +80,7 @@ Lemma GPS_aSP_SWWrite IP IPC l κ q R o t s s' v v' γ tid E
   {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
       ∗ ▷ (if decide (AcqRel ⊑ o)%stdpp then WVS else △{tid} WVS)
       ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ IPC l γ t s v ∗ R) }}}
-    Write o #l v' in tid @ E
+    Write o #l v' @ tid; E
   {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_aSP_Writer IP IPC l κ t' s' v' γ
       ∗ (q).[κ] ∗ R }}}.
 Proof.
@@ -102,7 +102,7 @@ Lemma GPS_aSP_SWWrite_rel IP IPC l κ q Q Q1 Q2 t s s' v v' γ tid E
                      |={E ∖ ↑N}=> (IP true l γ t' s' v' ∗ Q t'))%I in
   {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aSP_Writer IP IPC l κ t s v γ
       ∗ ▷ WVS ∗ ▷ <obj> (IP true l γ t s v ={E ∖ ↑N}=∗ Q1 ∗ Q2) }}}
-    #l <-ʳᵉˡ v' in tid @ E
+    #l <-ʳᵉˡ v' @ tid; E
   {{{ t', RET #☠; ⌜(t < t')%positive⌝ ∗ GPS_aSP_Reader IP IPC l κ t' s' v' γ
       ∗ (q).[κ] ∗ Q t' }}}.
 Proof.
@@ -142,7 +142,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_weak
       ∗ (▷ VSC)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then P  else △{tid} P) }}}
-    CAS #l #vr vw orf or ow in tid @ E
+    CAS #l #vr vw orf or ow @ tid; E
   {{{ (b: bool) t' s' (v': lit), RET #b;
       (q).[κ] ∗ ⌜s ⊑ s'⌝
       ∗ ( (⌜b = true  ∧ v' = LitInt vr ∧ (t < t')%positive⌝
@@ -191,7 +191,7 @@ Lemma GPS_aSP_SharedWriter_CAS_int_strong
       ∗ (▷ VSC)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then P  else △{tid} P) }}}
-    CAS #l #vr vw orf or ow in tid @ E
+    CAS #l #vr vw orf or ow @ tid; E
   {{{ (b: bool) t' s' (v': lit), RET #b;
       (q).[κ] ∗ ⌜s ⊑ s'⌝
       ∗ ( (⌜b = true  ∧ v' = LitInt vr ∧ (t < t')%positive⌝
@@ -282,7 +282,7 @@ Lemma GPS_aPP_Read IP l κ q R (o: memOrder) t s v γ tid E
                         IP false l γ t' s' v' ∗ R t' s' v') ∧
                     (IP true l γ t' s' v' ={E ∖ ↑N}=∗
                         IP true l γ t' s' v' ∗ R t' s' v'))) }}}
-    Read o #l in tid @ E
+    Read o #l @ tid; E
   {{{ t' s' v', RET v'; ⌜s ⊑ s' ∧ t ⊑ t'⌝ ∗ GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ]
       ∗ if decide (AcqRel ⊑ o)%stdpp then R t' s' v' else ▽{tid} R t' s' v' }}}.
 Proof.
@@ -304,7 +304,7 @@ Lemma GPS_aPP_Write IP l κ q (o: memOrder) t v v' s s' γ tid E
           GPS_PP_Local l t' s' v' γ ={E ∖ ↑N}=∗ IP true l γ t' s' v')%I in
   {{{ ⎡ lft_ctx ⎤ ∗ (q).[κ] ∗ GPS_aPP IP l κ t s v γ
       ∗ ▷ if decide (AcqRel ⊑ o)%stdpp then VS else △{tid} VS }}}
-    Write o #l v' in tid @ E
+    Write o #l v' @ tid; E
   {{{ t', RET #☠; GPS_aPP IP l κ t' s' v' γ ∗ (q).[κ] }}}.
 Proof.
   iIntros (VS Φ) "(#LFT & Htok & #[Hlc Hshr] & VS) Post".
@@ -341,7 +341,7 @@ Lemma GPS_aPP_CAS_int_simple IP l κ q t s v (vr: Z) (vw: val) orf or ow γ
       ∗ ▷ VSC
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then VS else △{tid} VS)
       ∗ (if decide (AcqRel ⊑ ow)%stdpp then P  else △{tid} P ) }}}
-    CAS #l #vr vw orf or ow in tid @ E
+    CAS #l #vr vw orf or ow @ tid; E
   {{{ (b: bool) t' s' (v': lit), RET #b;
         (q).[κ] ∗ ⌜s ⊑ s'⌝
         ∗ ( (⌜b = true  ∧ v' = LitInt vr ∧ (t < t')%positive⌝
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index d6923a3111fdcba2cf1d405265fcdc964b687381..6ce090e36765ea0d031fd1d3c962c0af913a4538 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -25,7 +25,7 @@ Section cont_context.
     let '(k ◁cont(L, T)) := x in
     (∀ args, na_own tid top -∗
          llctx_interp qmax L -∗ tctx_interp tid (T args) -∗
-         WP k (base.of_val <$> (args : list _)) in tid
+         WP k (base.of_val <$> (args : list _)) @ tid; ⊤
            {{ _, cont_postcondition }})%I.
   Definition cctx_interp (tid : type.thread_id) (qmax: Qp) (C : cctx) : vProp Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid qmax x)%I.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index efef50ee926c5620d42dccf5a18d3a61770accf7..3faa1a71b9a9594719ec88e4ea6f5a6e3b3a1521 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -248,8 +248,8 @@ Section typing.
                    tctx_elt_interp tid y) -∗
     (∀ ret, na_own tid top -∗ llctx_interp_noend qmax L qL -∗ qκs.[lft_intersect_list κs] -∗
              (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
-             WP k [of_val ret] in tid {{ _, cont_postcondition }}) -∗
-    WP (call: p ps → k) in tid {{ _, cont_postcondition }}.
+             WP k [of_val ret] @ tid; ⊤ {{ _, cont_postcondition }}) -∗
+    WP (call: p ps → k) @ tid; ⊤ {{ _, cont_postcondition }}.
   Proof.
     iIntros (HE [k' <-]) "#LFT #HE Htl HL Hκs Hf Hargs Hk".
     wp_apply (wp_hasty with "Hf"); [done|]. iIntros (v) "% Hf".
@@ -318,8 +318,8 @@ Section typing.
                    tctx_elt_interp tid y) -∗
     (∀ ret, na_own tid top -∗ qκs.[lft_intersect_list κs] -∗
              (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
-             WP k [of_val ret] in tid {{ _, cont_postcondition }}) -∗
-    WP (call: f ps → k) in tid {{ _, cont_postcondition }}.
+             WP k [of_val ret] @ tid; ⊤ {{ _, cont_postcondition }}) -∗
+    WP (call: f ps → k) @ tid; ⊤ {{ _, cont_postcondition }}.
   Proof.
     iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk". rewrite -tctx_hasty_val.
     iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index f23113f4a4e340f408eccaeaf633498f8a2b65ee..d3c5b1944760a3afdab496b5df74a22f4a6908a0 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -248,7 +248,7 @@ Section code.
   Lemma rc_check_unique ty F tid (l : loc) :
     ↑rc_invN ⊆ F →
     {{{ na_own tid F ∗ ty_own (rc ty) tid [ #l ] }}}
-    !#l in tid
+    !#l @ tid; ⊤
     {{{ strong, RET #(Zpos strong); l ↦ #(Zpos strong) ∗
         (((⌜strong = 1%positive⌝ ∗
            (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d7c12c479d433b83f36c1467bcc3c2ab145fe8ad..999858e7f99e9373d0b5915f83df42b0eeb374b4 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -14,7 +14,7 @@ Section typing.
                         (e : expr) : vPropI Σ :=
     (∀ tid (qmax : Qp), ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
                cctx_interp tid qmax C -∗ tctx_interp tid T -∗
-               WP e in tid {{ _, cont_postcondition }})%I.
+               WP e @ tid; ⊤ {{ _, cont_postcondition }})%I.
   Global Arguments typed_body _ _ _ _ _%E.
 
   Global Instance typed_body_llctx_permut E :
@@ -62,7 +62,7 @@ Section typing.
              (T1 : tctx) (e : expr) (T2 : val → tctx) : vPropI Σ :=
     (∀ tid qmax, ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid ⊤ -∗
               llctx_interp qmax L -∗ tctx_interp tid T1 -∗
-       WP e in tid {{ v, na_own tid ⊤ ∗
+       WP e @ tid; ⊤ {{ v, na_own tid ⊤ ∗
                          llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
   Global Arguments typed_instruction _ _ _ _%E _.
 
@@ -306,7 +306,7 @@ Section typing_rules.
     typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
     {{{ ⎡lft_ctx⎤ ∗ elctx_interp E ∗ na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
-      (p1 <-{n} !p2) in tid
+      (p1 <-{n} !p2) @ tid; ⊤
     {{{ RET #☠; na_own tid ⊤ ∗ llctx_interp_noend qmax L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index f45b11d1a605e9e0863a1a5dbe6d0adbc7a3cbb9..2cf6c9db2687f458b12125bd29174266075e516b 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -6,6 +6,8 @@ Set Default Proof Using "Type".
 Definition path := expr.
 Bind Scope expr_scope with path.
 
+Global Instance wp_path `{!noprolG Σ} : Wp (vPropI Σ) path val thread_id := wp'.
+
 (* TODO: Consider making this a pair of a path and the rest. We could
    then e.g. formulate tctx_elt_hasty_path more generally. *)
 Inductive tctx_elt `{!typeG Σ} : Type :=
@@ -37,7 +39,7 @@ Section type_context.
   Proof. destruct v. done. simpl. rewrite (decide_True_pi _). done. Qed.
 
   Lemma wp_eval_path E tid p v (SUB : ↑histN ⊆ E) :
-    eval_path p = Some v → ⊢ WP p in tid @ E {{ v', ⌜v' = v⌝ }}.
+    eval_path p = Some v → ⊢ WP p @ tid; E {{ v', ⌜v' = v⌝ }}.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
       try (intros <-%of_to_val; by iApply wp_value).
@@ -99,7 +101,7 @@ Section type_context.
   Lemma wp_hasty E tid p ty Φ (SUB : ↑histN ⊆ E) :
     tctx_elt_interp tid (p ◁ ty) -∗
     (∀ v, ⌜eval_path p = Some v⌝ -∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
-    WP p in tid @ E {{ Φ }}.
+    WP p @ tid; E {{ Φ }}.
   Proof.
     iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
     iApply (wp_wand with "[]"). { by iApply wp_eval_path. }