diff --git a/tests/telescopes.v b/tests/telescopes.v
index 401458967b8721101ef92d10f2ea5f81ff956c9e..73be62e134e7e736a8dbdb805265440251d55422 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -29,7 +29,7 @@ Section basic_tests.
   Proof. iIntros (H) "!%". done. Qed.
   Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT → PROP) :
     (∀.. x, <pers> (Φ x)) -∗ <pers> ∀.. x, Φ x.
-  Proof. iIntros "#H !#" (x). done. Qed.
+  Proof. iIntros "#H !>" (x). done. Qed.
   Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT → PROP) :
     (∃.. x, □ (Φ x)) -∗ □ ∃.. x, Φ x.
   Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 648da070094d980f4af3ade74125e58286d14526..8fb0f8590b853ae41f9bfdba8d531eb601f098df 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -60,7 +60,7 @@ Section instances.
   Proof.
     rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H".
     iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]".
-    iExists Q. iIntros "{$HQ} !# HQ". iExists x. by iApply "HΦ".
+    iExists Q. iIntros "{$HQ} !> HQ". iExists x. by iApply "HΦ".
   Qed.
 
   Global Instance big_sepL_laterable Ps :
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index d56b2ae6225d8a00d8108250589a5a41a9d11d3c..102024ff3eccef887fd563039ecd816be08e2f43 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -51,7 +51,7 @@ Section proof.
   Proof.
     iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
     iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
-    iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]";
+    iIntros "!> !>"; iSplit; iDestruct 1 as (b) "[Hl H]";
       iExists b; iFrame "Hl"; destruct b;
       first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
   Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index c6ce4c057d725059d083ebd6812f59680dbf6a9f..be61915fa83a00557e9f934db763c6b070a91659 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -75,7 +75,7 @@ Section proof.
   Proof.
     iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
     iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
-    iIntros "!> !#"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
+    iIntros "!> !>"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
       iExists o, n; iFrame "Ho Hn H●";
       (iDestruct "H" as "[[Hâ—¯ H]|Hâ—¯]"; [iLeft; iFrame "Hâ—¯"; by iApply "HR"|by iRight]).
   Qed.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 05f0a8f3b3a0e01cbeaa1549e446a9734ab50e2b..d601751b8f9b9f741d76fb00ec2955c4002ef380 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -229,7 +229,7 @@ Lemma wp_rec_löb s E f x e Φ Ψ :
 Proof.
   iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
   iApply lifting.wp_pure_step_later; first done.
-  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!#" (w) "HΨ".
+  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
   iApply ("IH" with "HΨ").
 Qed.