diff --git a/opam b/opam
index 3830f0367eecdacae52365a84aa0fd646ed247db..5bcd9528992d1c2121395137729bc212186d89f5 100644
--- a/opam
+++ b/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") }
 ]
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 60be506be7cdafd528e641c0d6971e99ec913271..45ba12f1c639c29461594cb072f98291bd21ed2e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/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]".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 580275adacc4c2ef17c032ee5cbfabc043b6beb4..ae52a295ecea8a345fd4e50e11455266f7cb1194 100644
--- a/theories/lifetime/model/definitions.v
+++ b/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.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 25519cbb720858196889b39d116d03b387787c0b..19ca418de968ba94d41eac81ba5ecad6aed10cf0 100644
--- a/theories/lifetime/model/primitive.v
+++ b/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.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e7500c0fef91331c921436c71598328e472ab5f2..b0c84dd1c121a395969f8d0a0ba7d3d169f6fe39 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/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.