From 5734a7804c581a7fabf68a59e6ca79db49074015 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 11 Feb 2020 23:23:52 +0100
Subject: [PATCH] bump gpfsl

---
 opam                                      | 2 +-
 theories/typing/lib/refcell/refmut_code.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index d0738983..6defee7d 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 3f73f40b..8863fcbc 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.
-- 
GitLab