From 161fccaa8172fb57fd44c102d7b98ea42c518a15 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Nov 2019 11:19:11 +0100
Subject: [PATCH] Bump Iris (`iPoseProof` changes).
---
opam | 2 +-
theories/lifetime/model/accessors.v | 2 +-
theories/typing/soundness.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index 27f078c2..9c3d0ce5 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.2019-11-11.0.60647cc2") | (= "dev") }
+ "coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index bd164ce8..3fa9066e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -181,7 +181,7 @@ Proof.
solve_ndisj. by rewrite lookup_fmap EQB.
iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
- iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
+ iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
- apply delete_singleton_local_update, _.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 84f4c4d3..6157b9a8 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -38,7 +38,7 @@ Section type_soundness.
iMod lft_init as (?) "#LFT". done.
iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
wp_bind (of_val main). iApply (wp_wand with "[Htl]").
- iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []").
+ iApply (Hmain Htype [] [] $! tid with "LFT [] Htl [] []").
{ by rewrite /elctx_interp big_sepL_nil. }
{ by rewrite /llctx_interp big_sepL_nil. }
{ by rewrite tctx_interp_nil. }
--
GitLab