From 9843e3f096b1672094a55a2fa751f2d322a94386 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 23 Feb 2018 15:45:00 +0100
Subject: [PATCH] Bump Iris, fix build.
---
opam | 2 +-
theories/lifetime/model/borrow.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 32a6c2a3..55db4e7d 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 ce5f8124..5d3f2864 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.
--
GitLab