From 962637df10a879ac4b1b9d523854d6fa4c9e8fb4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Apr 2020 17:01:07 +0200
Subject: [PATCH] avoid deprecated !#

---
 tests/telescopes.v                   | 2 +-
 theories/bi/lib/laterable.v          | 2 +-
 theories/heap_lang/lib/spin_lock.v   | 2 +-
 theories/heap_lang/lib/ticket_lock.v | 2 +-
 theories/heap_lang/lifting.v         | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index 401458967..73be62e13 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 648da0700..8fb0f8590 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 d56b2ae62..102024ff3 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 c6ce4c057..be61915fa 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 05f0a8f3b..d601751b8 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.
 
-- 
GitLab