diff --git a/opam b/opam
index b7703746b2e8d9f142e97b80f2344e11d9eff995..d0738983d2ef0cc4caef49b5ac0c79d4bca492ed 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 e9206f03a8589208090c09eac69efcd277ad7f0f..5dcefa91ad98d79ed6a20ceaf6933ca6a8eda18e 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".