From 0432071542b81fe3b1cfcd949304b57f82001a6a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 23 Feb 2018 12:43:02 +0100
Subject: [PATCH] Bump iris.

---
 opam           | 2 +-
 theories/rsl.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index b04df149..4141be77 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 802845a5..89a49b8d 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]").
-- 
GitLab