Fix build, bump gpfsl/iris

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-29.0.a1b7d4e9") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-09-15.0.a4aa00fe") | (= "dev") }
 ]

theories/lifetime/model/boxes.v

@@ -144,10 +144,10 @@ Lemma slice_delete_empty q f P Q γ :
     ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
 Proof.
   iIntros (?) "#[HγQ _] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
-  iDestruct (big_opM_delete _ f _ None with "Hf") as "[[_ [HΦ _]] Hf]"; [done|].
+  iDestruct (big_sepM_delete _ f _ None with "Hf") as "[[_ [HΦ _]] Hf]"; [done|].
   set (P' := ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I). iExists P'. iSplitR "Hf"; iNext.
   - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto. iNext.
-    iRewrite "HeqP". iRewrite "HeqQ". rewrite big_opM_delete //.
+    iRewrite "HeqP". iRewrite "HeqQ". rewrite big_sepM_delete //.
   - iExists Φ; eauto.
 Qed.
 
@@ -158,13 +158,13 @@ Lemma slice_fill E q f γ P Q V :
 Proof.
   iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (o') "[>Hγ _]" "Hclose".
-  iDestruct (big_opM_delete _ f _ None with "Hf")
+  iDestruct (big_sepM_delete _ f _ None with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iMod (box_own_auth_update γ o' None (Some $ to_latT V) with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iMod ("Hclose" with "[Hγ HQ]") as "_"; [iNext; iExists (Some $ to_latT V); by iFrame|].
   iModIntro; iNext; iExists Φ; iSplit.
-  - by rewrite big_opM_insert_override.
-  - rewrite -insert_delete big_opM_insert ?lookup_delete //. auto with iFrame.
+  - by rewrite big_sepM_insert_override.
+  - rewrite -insert_delete big_sepM_insert ?lookup_delete //. auto with iFrame.
 Qed.
 
 Lemma slice_empty E q f P Q γ V :
@@ -174,14 +174,14 @@ Lemma slice_empty E q f P Q γ V :
 Proof.
   iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (o) "[>Hγ HQ]" "Hclose".
-  iDestruct (big_opM_delete _ f with "Hf") as "[[>Hγ' #[HγΦ Hinv']] ?]"; [done|].
+  iDestruct (big_sepM_delete _ f with "Hf") as "[[>Hγ' #[HγΦ Hinv']] ?]"; [done|].
   iDestruct (box_own_auth_agree γ o (Some $ to_latT V) with "[-]") as %EQ; [by iFrame|].
   inversion_clear EQ. setoid_subst. iFrame "HQ".
   iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iMod ("Hclose" with "[Hγ]") as "_"; [iNext; iExists None; by repeat iSplit|].
   iModIntro; iNext; iExists Φ; iSplit.
-  - by rewrite big_opM_insert_override.
-  - rewrite -insert_delete big_opM_insert ?lookup_delete //. auto with iFrame.
+  - by rewrite big_sepM_insert_override.
+  - rewrite -insert_delete big_sepM_insert ?lookup_delete //. auto with iFrame.
 Qed.
 
 Lemma slice_insert_full E q f P Q V :
@@ -214,11 +214,11 @@ Lemma box_fill E f P V :
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR.
-  { iModIntro. iNext. iRewrite "HeqP". by rewrite big_opM_fmap. }
+  { iModIntro. iNext. iRewrite "HeqP". by rewrite big_sepM_fmap. }
   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 (big_sepM_fupd _ _ f).
+  rewrite -big_sepM_sep big_sepM_fmap; iApply (big_sepM_fupd _ _ f).
   iApply (@big_sepM_impl with "[$Hf]").
   iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
@@ -247,8 +247,8 @@ Proof.
     iFrame "HγΦ Hinv". by iApply "HΦ". }
   iModIntro; iSplitL "HΦ".
   - rewrite -big_sepM_later -monPred_at_big_sepM. iNext. by iRewrite "HeqP".
-  - iExists Φ; iSplit; [|by rewrite big_opM_fmap].
-    iNext. iRewrite "HeqP". by rewrite big_opM_fmap.
+  - iExists Φ; iSplit; [|by rewrite big_sepM_fmap].
+    iNext. iRewrite "HeqP". by rewrite big_sepM_fmap.
 Qed.
 
 Lemma slice_iff E q f P Q Q' γ o :