From 81cc44600d727b4ea6e6cbda15750997be7f54a7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Apr 2020 10:59:12 +0200
Subject: [PATCH] avoid (implicit) 'try'

---
 theories/base_logic/lib/gen_inv_heap.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index e022e2d77..02843da24 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -223,7 +223,7 @@ Section inv_heap.
         inv_mapsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
   Proof.
     iIntros (HN) "#Hinv".
-    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"=>//.
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
     iIntros "!>" (l v I) "Hl_inv".
     iDestruct "HP" as (h) "[H● HsepM]".
     iDestruct (inv_mapsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
@@ -262,11 +262,11 @@ Section inv_heap.
     ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
   Proof.
     iIntros (HN) "#Hinv Hl_inv".
-    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"=>//.
+    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
     iModIntro.
     iDestruct "HP" as (h) "[H● HsepM]".
     iDestruct (inv_mapsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
-    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"=>//.
+    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
     setoid_rewrite HI'.
     iExists _. iIntros "{$HI $Hl} Hl".
     iMod ("Hclose" with "[H● HsepM Hl]"); last done.
-- 
GitLab