From a3969eb5efd8d2ff44d9da9177ef797c070682c3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Jul 2020 14:42:36 +0200
Subject: [PATCH] also avoid '!#'

---
 theories/base_logic/lib/invariants.v | 4 ++--
 theories/base_logic/lib/viewshifts.v | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 43b606651..9362abc84 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 7401005bd..d94376bc7 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.
-- 
GitLab