From 5378cb1153a6046be0fa333baed0fee2612bc866 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 25 Aug 2019 21:10:13 +0200
Subject: [PATCH] Bump.

---
 opam                            | 2 +-
 theories/lifetime/model/boxes.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index 0efbdaae..e0ba3491 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.2019-08-13.1.5876a5f6") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-08-25.0.4eb5203b") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 3091f461..bf0383e5 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -218,7 +218,7 @@ Proof.
   iAssert ([∗ map] γ↦_ ∈ f, ▷ Φ γ V)%I with "[HP]" as "HP'".
   { rewrite -big_sepM_later -monPred_at_big_sepM. iNext. by iRewrite "HeqP" in "HP". }
   iCombine "Hf" "HP'" as "Hf".
-  rewrite -big_sepM_sep big_opM_fmap; iApply (fupd_big_sepM _ _ f).
+  rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
   iApply (@big_sepM_impl with "[$Hf]").
   iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
@@ -235,7 +235,7 @@ Proof.
   iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ V) ∗
     [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
-  { rewrite -big_sepM_sep -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
+  { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
     iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (Ho : from_option (⊑ V) False o) by eauto.
     destruct o as [V'|]=>//. rewrite -Ho.
-- 
GitLab