diff --git a/opam b/opam
index 32a6c2a37b2987e569b24bf995a7cea05ab867a2..55db4e7d5cff2e71eee6b50e0ef3c3130bb4ecc2 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.2018-02-21.1") | (= "dev") }
+  "coq-iris" { (= "dev.2018-02-23.0") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index ce5f8124c5403e4db618dd5d8d23b770a41aac42..5d3f286498c222b9e16d57297f1b6254a7166d26 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -41,7 +41,7 @@ Proof.
       rewrite /lft_bor_alive. iExists _. iFrame "HboxB HB●".
       iApply @big_sepM_insert; first by destruct (B !! γB).
       simpl. iFrame. }
-    iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
+    iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
     + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
       iExists P. rewrite -uPred.iff_refl. auto.