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-21.1.ef511c16") | (= "dev") }
+  "coq-iris" { (= "dev.2019-03-04.1.a848ac3b") | (= "dev") }
 ]

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Λ. }