From 8e868ab45ee0e15b610f7e086dfc2c86e5f69607 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 4 Mar 2019 12:10:09 +0100
Subject: [PATCH] bump iris
---
opam | 2 +-
theories/lifetime/model/creation.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 5bcd9528..deef22a3 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-02-21.1.ef511c16") | (= "dev") }
+ "coq-iris" { (= "dev.2019-03-04.1.a848ac3b") | (= "dev") }
]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 9c336443..672bf284 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -111,7 +111,7 @@ Lemma lft_create E :
Proof.
iIntros (?) "#LFT".
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
- destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
+ destruct (exist_fresh (dom (gset atomic_lft) A)) as [Λ HΛ%not_elem_of_dom].
iMod (own_update with "HA") as "[HA HΛ]".
{ apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
by rewrite lookup_fmap HΛ. }
--
GitLab