diff --git a/opam.pins b/opam.pins
index 47804d3c16e251ff2fa80955b3d65167e7471625..ad60b637b1252cfed2b814cde2069041ce0ecc3a 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 26e93ebf7d4cfcd4c1c278c2e57ad0ae12a97ab6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4e1bdcc778381975fbcef1c24736ec384c5ba661
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 70f6f9069c405e64868a9cb9feb8b2948efe6ab0..c6bafa39836158d1f2143b26bd7c057ce0083030 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -592,7 +592,7 @@ Canonical Structure valC := leibnizC val.
 Canonical Structure exprC := leibnizC expr.
 
 (** Language *)
-Program Instance lrust_ectxi_lang: EctxiLanguage expr val ectx_item state :=
+Program Instance lrust_ectxi_lang : EctxiLanguage expr val ectx_item state :=
   {| ectxi_language.of_val := of_val;
      ectxi_language.to_val := to_val;
      ectxi_language.fill_item := fill_item;
@@ -605,14 +605,11 @@ Canonical Structure lrust_lang := ectx_lang expr.
 (* Lemmas about the language. *)
 Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
 Proof.
-  intros ??? Hstep. edestruct step_is_head as (?&?&?&?); [..|by do 3 eexists|].
-  - done.
-  - clear. intros Ki K e' Heq (?&?&? & Hstep). destruct Ki; inversion Heq.
-    + destruct K as [|Ki K].
-      * simpl in *. subst. inversion Hstep.
-      * destruct Ki; simpl in *; done.
-    + destruct (of_val <$> vl); last done. destruct (fill K e'); done.
-  - by eapply stuck_not_head_step.
+  apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
+  apply prim_head_irreducible; unfold stuck_term.
+  - inversion 1.
+  - apply ectxi_language_sub_values.
+    intros [] ??; simplify_eq/=; eauto; discriminate_list.
 Qed.
 
 (* Define some derived forms *)
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 6cc6f95bddf46888244d815208fd880e2c9e425d..3321b135b6fd5cecc7a04f3c988545d9539c9a83 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -67,28 +67,19 @@ Definition nonracing_accesses (a1 a2 : access_kind * order) : Prop :=
   | _, _ => False
   end.
 
-Definition nonracing_threadpool (el : list expr) σ : Prop :=
+Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
   ∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
              nonracing_accesses a1 a2.
 
-Lemma next_access_head_head K e σ a l:
-  next_access_head (fill_item K e) σ a l → is_Some (to_val e).
-Proof.
-  destruct K; inversion 1; eauto.
-Qed.
-
 Lemma next_access_head_reductible_ctx e σ σ' a l K :
   next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
 Proof.
-  intros Ha. apply step_is_head.
-  - by destruct Ha.
-  - clear -Ha. intros Ki K e' Heq (?&?&?&Hstep).
-    subst e. apply next_access_head_head in Ha.
-    change to_val with ectxi_language.to_val in Ha.
-    rewrite fill_not_val in Ha. by eapply is_Some_None. by eapply val_stuck.
+  intros Hhead Hred. apply prim_head_reducible.
+  - eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
+  - apply ectxi_language_sub_values. intros [] ? ->; inversion Hhead; eauto.
 Qed.
 
-Definition head_reduce_not_to_stuck e σ :=
+Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
   ∀ e' σ' efs, ectx_language.head_step e σ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
 
 Lemma next_access_head_reducible_state e σ a l :
@@ -171,7 +162,7 @@ Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef :
 Proof.
   intros Hsafe Hi Hstep e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  { subst. intros (?&?&?&?). by eapply stuck_irreducible. }
   destruct (elem_of_list_split _ _ Hi) as (?&?&->).
   eapply Hsafe; last by (apply: fill_not_val; subst).
   - eapply rtc_l, rtc_l, rtc_refl.
@@ -188,7 +179,7 @@ Lemma safe_not_reduce_to_stuck el σ K e :
 Proof.
   intros Hsafe Hi e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  { subst. intros (?&?&?&?). by eapply stuck_irreducible. }
   destruct (elem_of_list_split _ _ Hi) as (?&?&->).
   eapply Hsafe; last by (apply: fill_not_val; subst).
   - eapply rtc_l, rtc_refl.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 299ae3f1bbcb83d9fc95239315ca0c4d3c033c99..73e0cd6f73cb5e33d8b9ab8ff40992117d4203c0 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -157,8 +157,7 @@ Proof.
     destruct e; simpl; try done; repeat (case_match; try done);
     inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
     rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
-  - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
-    apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
+  - apply ectxi_language_sub_values=> /= Ki e' Hfill.
     revert He. destruct e; simpl; try done; repeat (case_match; try done);
     rewrite ?bool_decide_spec;
     destruct Ki; inversion Hfill; subst; clear Hfill;
@@ -249,7 +248,7 @@ Ltac reshape_expr e tac :=
     end
   with go K e :=
   match e with
-  | _ => tac (reverse K) e
+  | _ => tac K e
   | BinOp ?op ?e1 ?e2 =>
      reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
   | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index a2792c74498a5968f9a9d8801eea333fe18777b9..ad0124a18a230d4d646d86a891bfdf6f2c150c27 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -130,7 +130,7 @@ Section frac_bor.
   Lemma frac_bor_fake E κ :
     ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &frac{κ}φ.
   Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT >"). done.
+    iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT [>]"); first done.
     by iApply (bor_fake with "LFT").
   Qed.
 End frac_bor.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 5b17cf61b42aa0ce31d5d6a551c2221494f101c8..17957f5ebdb2fafe6d89755f0a2d6736447c4bd7 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -66,7 +66,7 @@ Proof.
       iNext; iFrame "Hinv". rewrite /lft_inv. iRight. iSplit; auto. }
     iMod (fupd_intro_mask') as "Hclose"; last iModIntro; first solve_ndisj.
     iNext. iMod "Hclose" as "_".
-    iApply (bor_fake with "LFT >"); first done.
+    iApply (bor_fake with "LFT [>]"); first done.
     iApply (lft_incl_dead with "[] H†"); first done.
     by iApply (lft_intersect_mono with "Hκ⊑"). }
   rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 78a7bb2dffa60292af019ad00c038d53e4305a00..5d17cd6ef7c8f3f689fed1a1322ddd086626bd5b 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -46,7 +46,7 @@ Section na_bor.
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
     iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
     iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
-    iIntros "{$HP $Hnaown}!>HP Hnaown".
+    iIntros "{$HP $Hnaown} !> HP Hnaown".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
@@ -58,7 +58,7 @@ Section na_bor.
 
   Lemma na_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &na{κ,tid,N}P.
   Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_na with ">"). done.
+    iIntros (?) "#LFT#H†". iApply (bor_na with "[>]"); first done.
     by iApply (bor_fake with "LFT H†").
   Qed.
 End na_bor.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 083504bbce54d5fc02fa5a2a229ded4dcc7efe7a..863295a5a216e75be0aa6543bdb69ca73a7bce9f 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -86,14 +86,14 @@ Section shared_bors.
   Lemma shr_bor_fake E κ:
     ↑lftN ⊆ E → N ⊥ lftN → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,N}P.
   Proof.
-    iIntros (??) "#LFT#H†". iApply (bor_share with ">"); try done.
+    iIntros (??) "#LFT#H†". iApply (bor_share with "[>]"); try done.
     by iApply (bor_fake with "LFT H†").
   Qed.
 
   Lemma shr_bor_fake_lftN E κ:
     ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ,lftN}P.
   Proof.
-    iIntros (?) "#LFT#H†". iApply (bor_share_lftN with ">"); try done.
+    iIntros (?) "#LFT#H†". iApply (bor_share_lftN with "[>]"); try done.
     by iApply (bor_fake with "LFT H†").
   Qed.
 End shared_bors.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 8750b714cb43629b8e70b75fbc76e7ef331006f4..ca51e24e35fe73c8252265a1893e28b9bc900593 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -149,7 +149,7 @@ Section typing.
       iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
       iMod ("Hclose" with "HE'") as "HE".
       iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
-      iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] Htl HL >").
+      iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] Htl HL [> -]").
       { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 1f27369931496d337d6ab94b18789cae3ae487b8..de2276bc2a116ff5680316adcbf04cefda43e657 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -252,7 +252,7 @@ Section lft_contexts.
     iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
     iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗
       (q'.[foldr lft_intersect static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
-      with ">[HE HL1]" as "H".
+      with "[> HE HL1]" as "H".
     { move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
       iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
       - iExists 1%Qp. iFrame. iSplitR; last by auto. iApply lft_tok_static.
@@ -287,7 +287,7 @@ Section lft_contexts.
       by iApply elctx_interp_persist. by iApply llctx_interp_persist.
     iMod (Hal with "HE HL") as (q') "[Htok Hclose]". done.
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose']". done.
-    iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with ">").
+    iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with "[> -]").
     by iApply "Hclose'".
   Qed.
 
@@ -400,7 +400,7 @@ Section elctx_incl.
       iMod (Hxy with "HE HL HE1") as (qy) "[HE1 Hclose1]"; first done.
       iMod (Hyz with "HE HL HE1") as (qz) "[HE1 Hclose2]"; first done.
       iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
-      iApply ("Hclose1" with ">"). iApply "Hclose2". done.
+      iApply ("Hclose1" with "[> -]"). by iApply "Hclose2".
   Qed.
 
   Lemma elctx_incl_refl E' : elctx_incl E' E'.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index c9d54b7f42606cb8a7ee8a25dae0cdace258b913..03e6889d6e7e65de67bbe581694fec08f8e76ad8 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -102,7 +102,7 @@ Section rc.
         iMod (bor_sep with "LFT HX") as "[Hrc HX]"; first solve_ndisj.
         iMod (bor_sep with "LFT HX") as "[_ HX]"; first solve_ndisj.
         iMod (bor_sep with "LFT HX") as "[Hlft _]"; first solve_ndisj.
-        iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
+        iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "#Hlft".
         { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
         iMod (bor_na with "Hrc") as "$"; first solve_ndisj.
         by iFrame "#". }
@@ -309,8 +309,7 @@ Section code.
     iIntros (tid qE) "#LFT Hna HE HL Hk".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "[Hrcx [Hrc' Hx]]". rewrite [[rcx]]lock.
-    destruct x as [[|x|]|]; try done.
-    (* FIXME why is x printed in the code as "LitV x", not "#x"? *)
+    destruct x as [[|x|]|]; try done. simpl of_val. (* TODO: simpl unfolds too much *)
     iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[>Hx >SZ]".
     rewrite uninit_own. destruct vl as [|]; iDestruct "SZ" as %[=].
     destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
@@ -391,7 +390,7 @@ Section code.
     - iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & #Hν† & #Hshr & Hclose)".
       wp_op; intros Hc.
       { exfalso. move:Hc. move/Zpos_eq_iff. intros ->. exact: Pos.lt_irrefl. }
-      wp_if. iMod ("Hclose" with ">[$Hrc● $Hrc $Hna]") as "Hna"; first by eauto.
+      wp_if. iMod ("Hclose" with "[> $Hrc● $Hrc $Hna]") as "Hna"; first by eauto.
       iApply (type_type _ _ _ [ x ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
                                 rcx ◁ box (uninit 1);
                                 #rc' ◁ rc ty ]%TC
@@ -460,7 +459,7 @@ Section code.
     - iDestruct "Hproto" as (γ ν q q') "(#Hinv & Hrctok & Hrc● & Hν & _ & _ & Hclose)".
       wp_write. wp_op; intros Hc.
       { exfalso. move:Hc. move/Zpos_eq_iff. intros ->. exact: Pos.lt_irrefl. }
-      wp_if. iMod ("Hclose" $! (c-1)%positive q' with ">[Hrc● Hrctok Hrc Hν $Hna]") as "Hna".
+      wp_if. iMod ("Hclose" $! (c-1)%positive q' with "[> Hrc● Hrctok Hrc Hν $Hna]") as "Hna".
       { unlock. iMod (own_update_2 with "Hrc● Hrctok") as "$".
         { apply auth_update_dealloc. rewrite -{1}(Pplus_minus c 1%positive); last first.
           { apply Pos.lt_gt. done. }
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 839c173b979cbaf85a5ebb76675a9496d68d3c2f..e2f9c77105ac4456dd43381a15ebdbbca1c63282 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -55,7 +55,7 @@ Section ref.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
     iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
-    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
+    iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
     iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
   Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index ac4a31ed9431bb3394513286d7ba7cb02bcdfd8b..4d3ee9f1ee303cf89931e84eab66562f5161e98b 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -123,7 +123,7 @@ Section refcell.
       iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
-    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with ">[-Hclose]"
+    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 7ed5f2a2a006e76864f4dd57a39ad6e8c05cbfd6..5cac4cd58412846e7ae2aed41bf9a92bf3379d5e 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -100,7 +100,7 @@ Section refcell_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
-        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with ">[Hx']" as "[_ Hx']".
+        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
         iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
@@ -164,7 +164,7 @@ Section refcell_functions.
         first by iExists st; iFrame.
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
+              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
@@ -177,7 +177,7 @@ Section refcell_functions.
       iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
                        ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
                        own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
-        with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
+        with "[> Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
       { destruct st as [[agν [|[q n]|]]|]; try done.
         - iDestruct "Hst" as (ν) "(Hag & H† & #Hshr & Hst)".
           iDestruct "Hst" as (q') "(#Hqq' & [Hν1 Hν2])".
@@ -211,7 +211,7 @@ Section refcell_functions.
       iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
       iApply (type_type  _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
-              with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk");
+              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk");
         first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
@@ -285,7 +285,7 @@ Section refcell_functions.
         iApply "Hbh". rewrite -lft_dead_or. auto. }
       iApply (type_type _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
-              with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
@@ -299,7 +299,7 @@ Section refcell_functions.
         first by iExists st; iFrame.
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 22a39c2c4a50ec6486d3fd57f0d428bbe330d11c..be1a12e63ff4539b1caadd496bcf3ce49f47b5b3 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -36,7 +36,7 @@ Section refmut_functions.
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
          [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
-    iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
+    iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]%TC
@@ -138,7 +138,7 @@ Section refmut_functions.
     iApply (wp_step_fupd with "[H† Hν]");
       [done| |iApply ("H†" with "Hν")|]; first set_solver.
     wp_seq. iIntros "{Hb} Hb !>".
-    iMod ("Hcloseβ" with ">[H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
+    iMod ("Hcloseβ" with "[> H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
     { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
       apply cancel_local_update_empty, _. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index f8abf1333c5a1f4c8b984c2e01aefb1c4d2bd57b..049e5ce511eff50838d2077d003f0fa272fb9c19 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -118,7 +118,7 @@ Section rwlock.
       iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
-    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with ">[-Hclose]"
+    iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 95008d7f5e590a7ee213391684cea61476b23c1a..a8ecae408f1c991661d4d6fda0c14766ce56ce8b 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -99,11 +99,11 @@ Section rwlock_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
-        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with ">[Hx']" as "[_ Hx']".
+        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
         iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
-      - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try iDestruct "H" as "[]".
+      - iIntros "H". iDestruct "H" as ([|[[| |z]|]vl]) "[H↦ H]"; try done.
         rewrite heap_mapsto_vec_cons.
         iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
         iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
@@ -170,7 +170,7 @@ Section rwlock_functions.
     iModIntro. wp_let. wp_op=>Hm1; wp_if.
     - iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
-              with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
+              with "[] LFT Hna [> Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockreadguard α ty));
@@ -185,7 +185,7 @@ Section rwlock_functions.
                          ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
                          ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
-          with ">[Hlx Hownst Hst Hβtok2]"
+          with "[> Hlx Hownst Hst Hβtok2]"
           as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV & H†)".
         { destruct st' as [[|[[agν q] n]|]|]; try done.
           - iDestruct "Hst" as (ν q') "(Hag & #H† & Hh & #Hshr & #Hqq' & [Hν1 Hν2])".
@@ -221,7 +221,7 @@ Section rwlock_functions.
         iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
                      #lx ◁ rwlockreadguard α ty]%TC
-              with "[] LFT Hna >[HE] HL Hk"); first last.
+              with "[] LFT Hna [> HE] HL Hk"); first last.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                   tctx_hasty_val' //. iFrame.
           iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
@@ -283,7 +283,7 @@ Section rwlock_functions.
       iModIntro. iApply (wp_if _ false). iNext.
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2) ]%TC
-              with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
+              with "[] LFT Hna [> Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockwriteguard α ty));
@@ -297,7 +297,7 @@ Section rwlock_functions.
       iApply (type_type  _ _ _
                    [ x ◁ box (&shr{α}(rwlock ty)); r ◁ box (uninit 2);
                      #lx ◁ rwlockwriteguard α ty]%TC
-              with "[] LFT Hna >[HE] HL Hk"); first last.
+              with "[] LFT Hna [> HE] HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
       { rewrite {1}/elctx_interp big_sepL_singleton //. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d14f88a4827e900a82487900a7d9732affc84d42..6388002fa6c586dd4d1362ab65f707e6ac094855 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -49,7 +49,7 @@ Section rwlockreadguard.
     iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
     iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
-    iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
+    iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
     { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
     iExists _. iFrame "#". iApply ty_shr_mono; last done.
     iApply lft_intersect_mono; last done. iApply lft_incl_refl.
@@ -87,7 +87,7 @@ Section rwlockreadguard.
         iApply lft_intersect_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.
       + iApply (shr_bor_iff with "[] Hinv").
-        iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
+        iIntros "!> !#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
     - iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
       iFrame. iApply ty_shr_mono; last by iApply "Hs".
       iApply lft_intersect_mono. done. iApply lft_incl_refl.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index af415324ecfedaf13dee3cbcddf1968925c75de1..d46cf2071e319bcf75d814de68dd9b14e0d5d478 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -124,7 +124,7 @@ Section rwlockwriteguard_functions.
     wp_bind (#lx' <-ˢᶜ #0)%E.
     iMod (shr_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
     iDestruct "INV" as (st) "(H↦ & H● & INV)". wp_write.
-    iMod ("Hcloseβ" with ">[H↦ H● H◯ INV Hx']") as "Hβ".
+    iMod ("Hcloseβ" with "[> H↦ H● H◯ INV Hx']") as "Hβ".
     { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> &
          [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2;
       last by destruct (exclusive_included _ _ Hle).
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index cddd811915349b9d0d5d100c2486a3a6dd091155..72f5e56bc221503c83d022b51f19bd462c943c46 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -172,7 +172,7 @@ Section typing_rules.
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono (↑lftN)); first done.
     iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
-    iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC >").
+    iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
 
@@ -262,7 +262,7 @@ Section typing_rules.
       as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
     iDestruct (ty_size_eq with "Hown2") as "#>%". subst v1 v2. iApply wp_fupd.
     iApply (wp_memcpy with "[$Hl1 $Hl2]"); try congruence; [].
-    iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with ">"). rewrite !tctx_hasty_val' //.
+    iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with "[> -]"). rewrite !tctx_hasty_val' //.
     iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
     { iExists _. iFrame. }
     iMod ("Hcl2" with "Hl2") as "($ & $ & $ & $)". done.