From 9dc14fb59f53470d241af57d51cd88c55538ce21 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 11:30:29 +0200
Subject: [PATCH] should fix the error

---
 theories/typing/lib/rc/rc.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index cb61f148..bf871939 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1066,7 +1066,7 @@ Section code.
         - iMod ("Hclose2" $! (shift_loc l 2 ↦∗: ty.(ty_own) tid)%I
             with "[Hrc' Hl1 Hl2 Hl†] Hl3") as "[Hty Hβ]"; first auto.
           { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton /=.
-            auto with iFrame. }
+            iFrame. simpl. auto with iFrame. }
           by iApply (ty_share with "LFT Hty Hβ").
         - iDestruct "Hty" as (γ ν q') "(Hpersist & Hown & Hν)".
           iDestruct "Hpersist" as (ty') "(Hty' & ? & #[?|Hν†] & ?)";
-- 
GitLab