diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 43b606651278774da08f714772377f12f531dad7..9362abc84e49e137ca3fe946a10cc5ae13799f31 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -137,7 +137,7 @@ Section inv.
     ↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
     inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
   Proof.
-    rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !#"; iIntros (E ?).
+    rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
     iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
     iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
     iMod (fupd_intro_mask' _ (E ∖ ↑N)) as "Hclose"; first set_solver.
@@ -149,7 +149,7 @@ Section inv.
     □ (P -∗ P ∗ P) -∗
     inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
   Proof.
-    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !#" (E ?).
+    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
     iMod ("HinvP" with "[//]") as "[HP HcloseP]".
     iDestruct ("HPdup" with "HP") as "[$ HP]".
     iMod ("HcloseP" with "HP") as %_.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 7401005bd150ca72c554a4008ca7a212998ca096..d94376bc77d5d956fc080c3089f0598ab4fcae7c 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -82,10 +82,10 @@ Lemma vs_inv_acc N E P :
   ⊢ inv N P ={E,E∖↑N}=> ▷ P ∗ ∃ R, R ∗ (R ∗ ▷ P ={E∖↑N,E}=> True).
 Proof.
   (* FIXME: scope printing is weird, there are [%stdpp]. *)
-  iIntros (?) "!# #Hinv".
+  iIntros (?) "!> #Hinv".
   iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done.
   iModIntro. iExists (▷ P ={E ∖ ↑N,E}=∗ True)%I. iFrame.
-  iIntros "!# [Hclose HP]". iMod ("Hclose" with "HP"). done.
+  iIntros "!> [Hclose HP]". iMod ("Hclose" with "HP"). done.
 Qed.
 
 Lemma vs_alloc N P : ⊢ ▷ P ={↑N}=> inv N P.