diff --git a/opam b/opam
index b04df149f81906206b06bfb05b02dfb116783090..4141be77f1b26f0d9f65ac82ea71d1734bfd2698 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-02-21.8") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-02-23.1") | (= "dev") }
 ]
diff --git a/theories/rsl.v b/theories/rsl.v
index 802845a5c04ade0a6d640bc4691ba19fb945cf7d..89a49b8df0e261077fd93c27bf66ea6024414e0e 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -934,8 +934,8 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
       iSplitR ""; last iSplitL "".
       + rewrite /RSLInv /sts_inv.
         iExists j, γ. iModIntro. iSplitL ""; first by iNext.
-        iExists s'. rewrite /rsl_inv /s'. iFrame "Own Hist'". iSplit; first auto.
-        iSplitR "ressD ress2"; [|iSplitR "ress2"; [|done]]; last first; iNext; iNext.
+        iExists s'. iFrame "Own Hist' ress2".
+        iNext. iSplit; first auto. iNext. iSplitR "ressD"; last first.
         * iApply (big_sepS_subseteq _ _ h' with "[$ressD]").
           by rewrite H11 union_comm_L.
         * iApply (big_sepS_subseteq _ _ (gblock_ends l h') with "[$ress]").