From 181d71116ceb172a74b697ddd026af961e09c0a6 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 4 Feb 2020 11:22:56 +0100
Subject: [PATCH] bump gpfsl

---
 opam                            | 2 +-
 theories/lifetime/frac_borrow.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index b7703746..d0738983 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2020-01-18.1.38a1445a") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-02-03.1.4594b3d4") | (= "dev") }
 ]
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e9206f03..5dcefa91 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -158,7 +158,7 @@ Section frac_bor.
       - destruct (decide (0 < qφ1)%Qc); [|done]. iCombine "HV HVb" as "HH".
         iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
         iApply (monPred_in_elim with "HVV"). iFrame. }
-    rewrite -Hqκ'. iClear "Hκκ' HV". clear dependent qφ0' qtok qφ1 Vb qφ0 V.
+    rewrite -Hqκ'. iClear "Hκκ' HV HVVb". clear dependent qφ0' qtok qφ1 Vb qφ0 V.
     iIntros "!> Hφ". iApply ("Hclose" with "[>-]"). clear κ.
     iMod (in_at_bor_acc with "LFT Hshr Hκ1") as (Vb) "[H Hclose']"; [done|].
     iCombine "H HV0" as "HH".
-- 
GitLab