diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index b0bb09df68d05267839ff444ff96abb93dd95b7c..f971580a987be3143201b9befedb5b1866684a38 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -150,7 +150,7 @@ Section tests.
       AllocN #n #0
     {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}%I.
   Proof.
-    iIntros (? ?) "!# _ HΦ".
+    iIntros (? ?) "!> _ HΦ".
     wp_alloc l as "?"; first done.
     by iApply "HΦ".
   Qed.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 5dad15580fb9025d8518a9e5a269191895c350ce..ac07123e5b71d5409f21fb20a5386a39eef830e7 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -77,7 +77,7 @@ Section list_reverse.
   Lemma rev_acc_ht hd acc xs ys :
     {{ is_list hd xs ∗ is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
   Proof.
-    iIntros "!# [Hxs Hys]".
+    iIntros "!> [Hxs Hys]".
     iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
     destruct xs as [|x xs]; iSimplifyEq.
     - (* nil *) by wp_match.
@@ -91,7 +91,7 @@ Section list_reverse.
   Lemma rev_ht hd xs :
     {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
   Proof.
-    iIntros "!# Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
+    iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
     iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
   Qed.
 End list_reverse.
@@ -204,7 +204,7 @@ Section counter_proof.
   Lemma newcounter_spec :
     {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
   Proof.
-    iIntros "!# _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
@@ -216,7 +216,7 @@ Section counter_proof.
   Lemma incr_spec l n :
     {{ C l n }} incr #l {{ v, ⌜v = #()⌝ ∧ C l (S n) }}.
   Proof.
-    iIntros "!# Hl /=". iLöb as "IH". wp_rec.
+    iIntros "!> Hl /=". iLöb as "IH". wp_rec.
     iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
     wp_bind (! _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c) "[Hl Hγ]".
@@ -241,7 +241,7 @@ Section counter_proof.
   Lemma read_spec l n :
     {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
   Proof.
-    iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
+    iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
     rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
     iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 03441f82772f02a2ec5cb5b267aaf43c67abb602..89ad969fba02b19723340b5f81f9069eb12376ab 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -52,7 +52,7 @@ Proof.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   wp_pures. iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
+  - iIntros (n) "!>". wp_lam. wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
@@ -60,7 +60,7 @@ Proof.
       iNext; iRight; iExists n; by iFrame.
     + wp_cmpxchg_fail. iModIntro. iSplitL; last (wp_pures; by eauto).
       rewrite /one_shot_inv; eauto 10.
-  - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
+  - iIntros "!> /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ ((⌜v = NONEV⌝ ∗ own γ Pending) ∨
        ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
@@ -74,7 +74,7 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_pures. iIntros "!#". wp_lam.
+    iModIntro. wp_pures. iIntros "!>". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
       subst; wp_match; [done|].
     wp_bind (! _)%E.
@@ -94,9 +94,9 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
       {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
-  iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
-  - iIntros (n) "!# _". wp_apply "Hf1".
-  - iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
+  iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
+  - iIntros (n) "!> _". wp_apply "Hf1".
+  - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
 Qed.
 End proof.
 
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 5a065a01fcf26eea56a1fc8f3fd556a68f897afb..6ad376e9ee63497d598c45cd0de4fee436773be7 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -68,7 +68,7 @@ Proof.
   { iNext. iLeft. by iFrame. }
   wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
   iSplitL; first done. iSplit.
-  - iIntros (n) "!# Hγ1". wp_pures.
+  - iIntros (n) "!> Hγ1". wp_pures.
     iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
     iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
     + iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
@@ -76,7 +76,7 @@ Proof.
       wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
       iNext; iRight; iExists n; by iFrame.
     + by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
-  - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
+  - iIntros "!> /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".
     iAssert (∃ v, l ↦ v ∗ (⌜v = NONEV⌝ ∗ own γ (Pending (1/2)%Qp) ∨
        ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
@@ -90,7 +90,7 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_pures. iIntros "!#". wp_lam. wp_bind (! _)%E.
+    iModIntro. wp_pures. iIntros "!>". wp_lam. wp_bind (! _)%E.
     iInv N as "Hinv".
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";
@@ -111,10 +111,10 @@ Lemma ht_one_shot (Φ : val → iProp Σ) :
       {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
-  iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
+  iIntros "!> _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
   iExists T. iFrame "HT". iSplit.
-  - iIntros (n) "!# HT". wp_apply "Hf1". done.
-  - iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
+  - iIntros (n) "!> HT". wp_apply "Hf1". done.
+  - iIntros "!> _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !> _".
 Qed.
 End proof.
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 735c423a3c13d09ad32c6d0eb73a5d9242b3a331..b41edc481b33abee85bdff9663bdd11f1b8e4021 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -416,7 +416,7 @@ Proof. iIntros (Q R) "$ _ $". Qed.
 
 Lemma test_iNext_iRewrite P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
-  iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
+  iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
 
 Lemma test_iIntros_modalities `(!Absorbing P) :
@@ -432,7 +432,7 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
 Lemma test_iNext_affine P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
-Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
+Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
   □ P -∗ <pers> Q → R -∗ <pers> <affine> <affine> P ∗ □ Q.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 3bfbc2ee5943fdb4de3c5a491cf707f9384d3cf4..39fabcd8d975a48aba36e52c46bb26218faf3dad 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -16,7 +16,7 @@ Section base_logic_tests.
       ▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌝ ↔ P3 n))) -∗
       ▷ ⌜x = 0⌝ ∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)))%I.
   Proof.
-    iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
+    iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
     { iLeft. by iNext. }
     iRight.
     iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 0205c03a397a6d45dfed2c42339156610151e9bb..d247efe8fb72cfaba19274ffafb0cb69d566c8ad 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -212,7 +212,7 @@ Proof.
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
   iApply (@big_sepM_impl with "Hf").
-  iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+  iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]".
   iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
   iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
@@ -228,7 +228,7 @@ Proof.
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯E false) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
-    iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
+    iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
     iInv N as (b) "[>Hγ HΦ]".
     iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index a5c376e163eb76c3fae34bee4c2ccc2d331456bf..12cbff8f3d0b0c6b5dc0ad85c7b4ed4775b6bfce 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -45,7 +45,7 @@ Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
 Proof.
   iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
   iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
-  iApply vs_impl. iIntros "!# HP". by iApply HPQ.
+  iApply vs_impl. iIntros "!> HP". by iApply HPQ.
 Qed.
 
 Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 337e27bfdb96a0f74e5fc7e8db547fb9edefec82..aa807e2211ea1a074e5bd03c6648c78580416faa 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -109,7 +109,7 @@ Section inv.
   Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
   Proof.
     iIntros "#HPQ #HI". iApply (inv_alter with "HI").
-    iIntros "!> !# HP". iSplitL "HP".
+    iIntros "!> !> HP". iSplitL "HP".
     - by iApply "HPQ".
     - iIntros "HQ". by iApply "HPQ".
   Qed.
@@ -169,7 +169,7 @@ Section inv.
   Lemma inv_sep_l N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
     iIntros "#HI". iApply inv_alter; eauto.
-    iIntros "!> !# [$ $] $".
+    iIntros "!> !> [$ $] $".
   Qed.
 
   Lemma inv_sep_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 5fe481ad4e9d12f28bbdf42319e525c34196462b..53163894186f53d9c92cd42945b4540adb8c2f31 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -40,45 +40,45 @@ Global Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1
 Proof. solve_proper. Qed.
 
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
-Proof. iIntros "!# []". Qed.
+Proof. iIntros "!> []". Qed.
 Lemma vs_timeless E P : Timeless P → ▷ P ={E}=> P.
-Proof. by iIntros (?) "!# > ?". Qed.
+Proof. by iIntros (?) "!> > ?". Qed.
 
 Lemma vs_transitive E1 E2 E3 P Q R :
   (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
 Proof.
-  iIntros "#[HvsP HvsQ] !# HP".
+  iIntros "#[HvsP HvsQ] !> HP".
   iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
 Qed.
 
 Lemma vs_reflexive E P : P ={E}=> P.
-Proof. by iIntros "!# HP". Qed.
+Proof. by iIntros "!> HP". Qed.
 
 Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
-Proof. iIntros "#HPQ !# HP". by iApply "HPQ". Qed.
+Proof. iIntros "#HPQ !> HP". by iApply "HPQ". Qed.
 
 Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ∗ P ={E1,E2}=> R ∗ Q.
-Proof. iIntros "#Hvs !# [$ HP]". by iApply "Hvs". Qed.
+Proof. iIntros "#Hvs !> [$ HP]". by iApply "Hvs". Qed.
 
 Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q ∗ R.
-Proof. iIntros "#Hvs !# [HP $]". by iApply "Hvs". Qed.
+Proof. iIntros "#Hvs !> [HP $]". by iApply "Hvs". Qed.
 
 Lemma vs_mask_frame_r E1 E2 Ef P Q :
   E1 ## Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
 Proof.
-  iIntros (?) "#Hvs !# HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
+  iIntros (?) "#Hvs !> HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
 Qed.
 
 Lemma vs_inv N E P Q R :
   ↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
 Proof.
-  iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
+  iIntros (?) "#[? Hvs] !> HP". iInv N as "HR" "Hclose".
   iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
   by iApply "Hclose".
 Qed.
 
 Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
-Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
+Proof. iIntros "!> HP". by iApply inv_alloc. Qed.
 
 Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
 Proof.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index eea2a3004a57bccb2ad561ef3158f755a6116640..638287c9b1db616c995e409c6651a05ad3159b27 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -76,7 +76,7 @@ Section definition.
     constructor.
     - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
       iApply (make_laterable_wand with "[] AU").
-      iIntros "!# AA". iApply (atomic_acc_wand with "[HP12] AA").
+      iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
     - intros ??. solve_proper.
   Qed.
@@ -255,8 +255,8 @@ Section lemmas.
     rewrite atomic_update_eq {2}/atomic_update_def /=.
     iIntros (Heo) "HAU".
     iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
-    iIntros "!# *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
-    iApply make_laterable_wand. iIntros "!#".
+    iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
+    iApply make_laterable_wand. iIntros "!>".
     iApply atomic_acc_mask_weaken. done.
   Qed.
 
@@ -300,8 +300,8 @@ Section lemmas.
   Proof.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
-    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
-    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!# >HQ".
+    iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
+    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> >HQ".
     iApply HAU. by iFrame.
   Qed.
 
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 594799bf0ca9717c298aa20b722f412a5729b7c1..ed3d464e9415bbeb3079342c957bf50b1447e7cb 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -43,7 +43,7 @@ Module savedprop. Section savedprop.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
   Proof.
-    iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'".
+    iIntros "#Hs !> #HA". iPoseProof "HA" as "HA'".
     iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
     iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
     { eauto. }
@@ -194,7 +194,7 @@ Module inv. Section inv.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
   Proof.
-    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
+    iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
     iDestruct "HA'" as (P) "#[HNP Hi']".
     iMod (saved_cast i (A i) P with "[]") as "HP".
     { eauto. }
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index df9083d3074b13826f3a8b456384cae00c85d1ff..3dc7fd525f86709e63a1162a56b08dae7b277404 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -38,15 +38,15 @@ Section least.
   Proof.
     rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
     iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
-    iIntros "!#" (y) "Hy". iApply ("Hy" with "[# //]").
+    iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
   Qed.
 
   Lemma least_fixpoint_unfold_1 x :
     bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
   Proof.
     iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
-    iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
-    iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2.
+    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
+    iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
   Qed.
 
   Corollary least_fixpoint_unfold x :
@@ -67,9 +67,9 @@ Section least.
   Proof.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
     { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
-      iIntros "!#" (y) "H". iSplit; first by iApply "HΦ".
+      iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
       iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[#] H").
-      by iIntros "!# * [_ ?]". }
+      by iIntros "!> * [_ ?]". }
     by setoid_rewrite and_elim_l.
   Qed.
 End least.
@@ -100,7 +100,7 @@ Section greatest.
   Proof.
     iDestruct 1 as (Φ) "[#Hincl HΦ]".
     iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]").
-    - iIntros "!#" (y) "Hy". iExists Φ. auto.
+    - iIntros "!>" (y) "Hy". iExists Φ. auto.
     - by iApply "Hincl".
   Qed.
 
@@ -108,8 +108,8 @@ Section greatest.
     F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
   Proof.
     iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
-    iSplit; last done. iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
-    iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
+    iSplit; last done. iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
+    iIntros "!>" (z) "?". by iApply greatest_fixpoint_unfold_1.
   Qed.
 
   Corollary greatest_fixpoint_unfold x :
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 155df72d47662abedd09a87cd84e585ab4f2aff8..7649218284d74d91056f776da374fcc4ba82af8a 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -20,14 +20,14 @@ Section instances.
   Global Instance later_laterable P : Laterable (â–· P).
   Proof.
     rewrite /Laterable. iIntros "HP". iExists P. iFrame.
-    iIntros "!# HP !>". done.
+    iIntros "!> HP !>". done.
   Qed.
 
   Global Instance timeless_laterable P :
     Timeless P → Laterable P.
   Proof.
     rewrite /Laterable. iIntros (?) "HP". iExists P%I. iFrame.
-    iSplitR; first by iNext. iIntros "!# >HP !>". done.
+    iSplitR; first by iNext. iIntros "!> >HP !>". done.
   Qed.
 
   (** This lemma is not very useful: It needs a strange assumption about
@@ -40,7 +40,7 @@ Section instances.
   Proof.
     rewrite /Laterable. iIntros (???) "#HP".
     iExists emp%I. iSplitL; first by iNext.
-    iIntros "!# >_". done.
+    iIntros "!> >_". done.
   Qed.
 
   Global Instance sep_laterable P Q :
@@ -50,7 +50,7 @@ Section instances.
     iDestruct (LP with "HP") as (P') "[HP' #HP]".
     iDestruct (LQ with "HQ") as (Q') "[HQ' #HQ]".
     iExists (P' ∗ Q')%I. iSplitL; first by iFrame.
-    iIntros "!# [HP' HQ']". iSplitL "HP'".
+    iIntros "!> [HP' HQ']". iSplitL "HP'".
     - iApply "HP". done.
     - iApply "HQ". done.
   Qed.
@@ -73,14 +73,14 @@ Section instances.
     □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
   Proof.
     iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
-    iExists P. iFrame. iIntros "!# HP". iApply "HQ". iApply "HQ1". done.
+    iExists P. iFrame. iIntros "!> HP". iApply "HQ". iApply "HQ1". done.
   Qed.
 
   Global Instance make_laterable_laterable Q :
     Laterable (make_laterable Q).
   Proof.
     rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
-    iExists P. iFrame. iIntros "!# HP !>". iExists P. by iFrame.
+    iExists P. iFrame. iIntros "!> HP !>". iExists P. by iFrame.
   Qed.
 
   Lemma make_laterable_elim Q :
@@ -95,7 +95,7 @@ Section instances.
   Proof.
     iIntros (?) "#HQ HP".
     iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
-    iFrame. iIntros "!# HP'". iApply "HQ". iApply "HPi". done.
+    iFrame. iIntros "!> HP'". iApply "HQ". iApply "HPi". done.
   Qed.
 
 End instances.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 3275afc7dbfe9084a9b9f17e207388a0e0855571..9776e183ebab776f6c1b80115743636ff774c33b 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -65,16 +65,16 @@ Global Instance ht_mono' s E :
 Proof. solve_proper. Qed.
 
 Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → {{ P }} e @ s; E {{ Φ }}.
-Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
+Proof. iIntros (Hwp) "!> HP". by iApply Hwp. Qed.
 
 Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌝ }}.
-Proof. iIntros "!# _". by iApply wp_value'. Qed.
+Proof. iIntros "!> _". by iApply wp_value'. Qed.
 
 Lemma ht_vs s E P P' Φ Φ' e :
   (P ={E}=> P') ∧ {{ P' }} e @ s; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
   ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof.
-  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
+  iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iMod ("Hvs" with "HP") as "HP".
   iApply wp_fupd. iApply (wp_wand with "(Hwp HP)").
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
@@ -83,7 +83,7 @@ Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ s; E1 {{ Φ }}.
 Proof.
-  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
+  iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iApply (wp_atomic _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
   iApply (wp_wand with "(Hwp HP)").
   iIntros (v) "Hv". by iApply "HΦ".
@@ -93,7 +93,7 @@ Lemma ht_bind `{!LanguageCtx K} s E P Φ Φ' e :
   {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
   ⊢ {{ P }} K e @ s; E {{ Φ' }}.
 Proof.
-  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
+  iIntros "[#Hwpe #HwpK] !> HP". iApply wp_bind.
   iApply (wp_wand with "(Hwpe HP)").
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
@@ -101,30 +101,30 @@ Qed.
 Lemma ht_stuck_weaken s E P Φ e :
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
 Proof.
-  by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp".
+  by iIntros "#Hwp !> ?"; iApply wp_stuck_weaken; iApply "Hwp".
 Qed.
 
 Lemma ht_mask_weaken s E1 E2 P Φ e :
   E1 ⊆ E2 → {{ P }} e @ s; E1 {{ Φ }} ⊢ {{ P }} e @ s; E2 {{ Φ }}.
 Proof.
-  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
+  iIntros (?) "#Hwp !> HP". iApply (wp_mask_mono _ E1 E2); try done.
   by iApply "Hwp".
 Qed.
 
 Lemma ht_frame_l s E P Φ R e :
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
-Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
+Proof. iIntros "#Hwp !> [$ HP]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_r s E P Φ R e :
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ R }} e @ s; E {{ v, Φ v ∗ R }}.
-Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
+Proof. iIntros "#Hwp !> [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
   (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
   ⊢ {{ R1 ∗ P }} e @ s; E1 {{ λ v, R2 ∗ Φ v }}.
 Proof.
-  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
+  iIntros (??) "[#Hvs #Hwp] !> [HR HP]".
   iApply (wp_frame_step_l _ E1 E2); try done.
   iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
 Qed.
@@ -134,7 +134,7 @@ Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
   (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
   ⊢ {{ P ∗ R1 }} e @ s; E1 {{ λ v, Φ v ∗ R2 }}.
 Proof.
-  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
+  iIntros (??) "[#Hvs #Hwp] !> [HP HR]".
   iApply (wp_frame_step_r _ E1 E2); try done.
   iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
 Qed.
@@ -143,7 +143,7 @@ Lemma ht_frame_step_l' s E P R e Φ :
   to_val e = None →
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
 Proof.
-  iIntros (?) "#Hwp !# [HR HP]".
+  iIntros (?) "#Hwp !> [HR HP]".
   iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
@@ -151,12 +151,12 @@ Lemma ht_frame_step_r' s E P Φ R e :
   to_val e = None →
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; E {{ v, Φ v ∗ R }}.
 Proof.
-  iIntros (?) "#Hwp !# [HP HR]".
+  iIntros (?) "#Hwp !> [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
 Lemma ht_exists (T : Type) s E (P : T → iProp Σ) Φ e :
   (∀ x, {{ P x }} e @ s; E {{ Φ }}) ⊢ {{ ∃ x, P x }} e @ s; E {{ Φ }}.
-Proof. iIntros "#HT !# HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
+Proof. iIntros "#HT !> HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
 
 End hoare.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 1f8d68102ef5d7e7898b208da88d424402a4684e..1dbbd877bea52a30cb46e23743adf481daa4fa40 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -43,13 +43,13 @@ Proof.
   assert (NonExpansive Ψ).
   { by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
   iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
-  iIntros "!#" (t') "H". by iApply "IH".
+  iIntros "!>" (t') "H". by iApply "IH".
 Qed.
 
 Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
 Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
-  iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
+  iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
   rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
   destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
   iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
@@ -59,9 +59,9 @@ Qed.
 Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
 Proof.
   iIntros "H1". iRevert (t2). iRevert (t1) "H1".
-  iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
+  iApply twptp_ind; iIntros "!>" (t1) "IH1". iIntros (t2) "H2".
   iRevert (t1) "IH1"; iRevert (t2) "H2".
-  iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
+  iApply twptp_ind; iIntros "!>" (t2) "IH2". iIntros (t1) "IH1".
   rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ2 n Hstep) "Hσ1".
   destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=.
   apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
@@ -74,7 +74,7 @@ Proof.
     + iMod ("IH1" with "[%] Hσ1") as (n2) "($ & Hσ & IH1 & _)"; first by econstructor.
       iAssert (twptp t2) with "[IH2]" as "Ht2".
       { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
-        iIntros "!# * [_ ?] //". }
+        iIntros "!> * [_ ?] //". }
       iModIntro. iExists n2. iFrame "Hσ".
       rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L. by iApply "IH1".
   - iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)"; first by econstructor.
@@ -85,7 +85,7 @@ Lemma twp_twptp s Φ e : WP e @ s; ⊤ [{ Φ }] -∗ twptp [e].
 Proof.
   iIntros "He". remember (⊤ : coPset) as E eqn:HE.
   iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
-  iIntros "!#" (e E Φ); iIntros "IH" (->).
+  iIntros "!>" (e E Φ); iIntros "IH" (->).
   rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ2' n Hstep) "Hσ1".
   destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
     simplify_eq/=; try discriminate_list.
@@ -106,7 +106,7 @@ Lemma twptp_total n σ t :
   state_interp σ [] n -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
   iIntros "Hσ Ht". iRevert (σ n) "Hσ". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ n) "Hσ".
+  iApply twptp_ind; iIntros "!>" (t) "IH"; iIntros (σ n) "Hσ".
   iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
   rewrite /twptp_pre.
   iMod ("IH" with "[% //] Hσ") as (n' ->) "[Hσ [H _]]".
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index f2bbcae8c907dacb4eb10f42d666cd9184a61223..0f25045e7acfdf3f1967e2a167dba87d5640a630 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -37,7 +37,7 @@ Proof.
   iMod ("Hwp" with "Hstep") as (?) "(Hσ & Hwp & Hfork)".
   iModIntro. iFrame "Hσ". iSplit; first done. iSplitL "Hwp".
   - by iApply "H".
-  - iApply (@big_sepL_impl with "Hfork"); iIntros "!#" (k e _) "Hwp".
+  - iApply (@big_sepL_impl with "Hfork"); iIntros "!>" (k e _) "Hwp".
     by iApply "H".
 Qed.
 
@@ -51,7 +51,7 @@ Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
   - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
-    iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
+    iApply twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
     rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
@@ -87,7 +87,7 @@ Proof.
   { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
   iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
-  iIntros "!#" ([[??] ?]) "H". by iApply "IH".
+  iIntros "!>" ([[??] ?]) "H". by iApply "IH".
 Qed.
 
 Global Instance twp_ne s E e n :
@@ -112,7 +112,7 @@ Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
 Proof.
   iIntros (? HE) "H HΦ". iRevert (E2 Ψ HE) "HΦ"; iRevert (e E1 Φ) "H".
   iApply twp_ind; first solve_proper.
-  iIntros "!#" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
+  iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1 κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
@@ -122,7 +122,7 @@ Proof.
   iMod "Hclose" as "_"; iModIntro.
   iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
-  - iApply (big_sepL_impl with "IHefs"); iIntros "!#" (k ef _) "[IH _]".
+  - iApply (big_sepL_impl with "IHefs"); iIntros "!>" (k ef _) "[IH _]".
     iApply "IH"; auto.
 Qed.
 
@@ -160,7 +160,7 @@ Proof.
     (∀ v, Φ' v -∗ WP K (of_val v) @ s; E [{ Φ }]) -∗ WP K e @ s; E [{ Φ }]).
   { iIntros (help Φ) "H". iApply (help with "H"); auto. }
   iIntros (Φ') "H". iRevert (e E Φ') "H". iApply twp_ind; first solve_proper.
-  iIntros "!#" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
+  iIntros "!>" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
   rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
   rewrite twp_unfold /twp_pre fill_not_val //.
@@ -180,10 +180,10 @@ Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
 Proof.
   iIntros "H". remember (K e) as e' eqn:He'.
   iRevert (e He'). iRevert (e' E Φ) "H". iApply twp_ind; first solve_proper.
-  iIntros "!#" (e' E1 Φ) "IH". iIntros (e ->).
+  iIntros "!>" (e' E1 Φ) "IH". iIntros (e ->).
   rewrite !twp_unfold {2}/twp_pre. destruct (to_val e) as [v|] eqn:He.
   { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
-    iApply (twp_pre_mono with "[] IH"). by iIntros "!#" (E e Φ') "[_ ?]". }
+    iApply (twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". }
   rewrite /twp_pre fill_not_val //.
   iIntros (σ1 κs n) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { destruct s; eauto using reducible_no_obs_fill. }
@@ -204,7 +204,7 @@ Proof.
   iApply step_fupd_intro; [set_solver+|]. iNext.
   iFrame "Hσ". iSplitL "H". by iApply "IH".
   iApply (@big_sepL_impl with "Hfork").
-  iIntros "!#" (k ef _) "H". by iApply "IH".
+  iIntros "!>" (k ef _) "H". by iApply "IH".
 Qed.
 
 (** * Derived rules *)
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 3752b6a0ef64e8523fb1dbdd398208f1e9fb3b4f..5bc2534b1352a99fc53423aba051ea24aaef84db 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -107,7 +107,7 @@ Proof.
   iMod "H" as "(Hσ & H & Hefs)".
   iMod "Hclose" as "_". iModIntro. iFrame "Hσ". iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
-  - iApply (big_sepL_impl with "Hefs"); iIntros "!#" (k ef _).
+  - iApply (big_sepL_impl with "Hefs"); iIntros "!>" (k ef _).
     iIntros "H". iApply ("IH" with "[] H"); auto.
 Qed.