From 5e73f2f92d08dd1e96adba053d1e91b1e9d69661 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 09:04:54 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/utils/contribution.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 16635d5..9d275d4 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/actris" ]
depends: [
- "coq-iris" { (= "dev.2020-10-10.0.cb8e35b8") | (= "dev") }
+ "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
]
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 4615bd9..3b7dec6 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -87,7 +87,7 @@ Section contribution.
Proof.
rewrite /server /client. iIntros "Hs Hc". case_decide; subst.
- iDestruct "Hs" as "(_ & _ & Hc')".
- by iDestruct (own_valid_2 with "Hc Hc'") as %?.
+ by iDestruct (own_valid_2 with "Hc Hc'") as %?%auth_frag_op_valid_1.
- iDestruct (own_valid_2 with "Hs Hc")
as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
--
GitLab