diff --git a/opam b/opam
index d0738983d2ef0cc4caef49b5ac0c79d4bca492ed..6defee7d413ede6e7d87971bc00c237cb6364fa4 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-02-03.1.4594b3d4") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-02-11.1.5b5497be") | (= "dev") }
 ]
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 3f73f40b02f0cee8286897400253d05f6ca6fb3c..8863fcbc9ede513de3c4d5b2cb82ffa47e075cab 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -80,8 +80,8 @@ Section refmut_functions.
     iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_sep with "LFT H") as "[H _]". done.
-    unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; [| |].
-    { split. by rewrite Qp_mult_1_r. apply _. } { done. }
+    unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
+    { split. by rewrite Qp_mult_1_r. apply _. }
     iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
     rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.