Bump Iris.

opam

@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
+  "coq-iris" { (= "dev.2019-02-21.1.ef511c16") | (= "dev") }
 ]

theories/lifetime/model/borrow_sep.v

@@ -78,9 +78,9 @@ Proof.
   iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
   iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
   iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
-    done. by apply gmultiset_union_subseteq_l.
+    done. by apply gmultiset_disj_union_subseteq_l.
   iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
-    done. by apply gmultiset_union_subseteq_r.
+    done. by apply gmultiset_disj_union_subseteq_r.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
   iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
   iDestruct "Hslice1" as (P') "[#HPP' Hslice1]".

theories/lifetime/model/definitions.v

@@ -17,7 +17,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Definition lft_intersect (κ κ' : lft) : lft := κ ∪ κ'.
+Definition lft_intersect (κ κ' : lft) : lft := κ ⊎ κ'.
 
 Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 

theories/lifetime/model/primitive.v

@@ -221,7 +221,7 @@ Proof. exists Λ. by rewrite lookup_insert. Qed.
 Lemma lft_dead_in_alive_in_union A κ κ' :
   lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
 Proof.
-  intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
+  intros (Λ & [Hin|Hin]%gmultiset_elem_of_disj_union & HΛ) Halive.
   - contradict HΛ. rewrite (Halive _ Hin). done.
   - exists Λ. auto.
 Qed.
@@ -264,7 +264,7 @@ Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
 Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
 
 Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
-Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
+Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
 
 Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
 Proof.

theories/lifetime/model/reborrow.v

@@ -173,9 +173,9 @@ Proof.
   rewrite /idx_bor /bor. destruct i as [κ0 i].
   iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
   iMod (raw_bor_shorten _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "Hbor";
-    [done|by apply gmultiset_union_subseteq_r|].
+    [done|by apply gmultiset_disj_union_subseteq_r|].
   iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
-    [done|by apply gmultiset_union_subset_l|].
+    [done|by apply gmultiset_disj_union_subset_l|].
   iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
     by iApply lft_intersect_mono.
 Qed.