diff --git a/opam b/opam
index 5bcd9528992d1c2121395137729bc212186d89f5..deef22a30fe08873954b8fb3f2b489962799ff10 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-21.1.ef511c16") | (= "dev") }
+  "coq-iris" { (= "dev.2019-03-04.1.a848ac3b") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 9c3364432bfa526c35a6c0c261c2ad5bb936c8e6..672bf284e96dd6f8a73123c3d6487267ac4eaed0 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -111,7 +111,7 @@ Lemma lft_create E :
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
+  destruct (exist_fresh (dom (gset atomic_lft) A)) as [Λ HΛ%not_elem_of_dom].
   iMod (own_update with "HA") as "[HA HΛ]".
   { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
     by rewrite lookup_fmap HΛ. }