From 232ef735fd3c4179de9f25974227c7d06bdc6adc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 09:18:32 +0200
Subject: [PATCH] Bump Iris.

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

diff --git a/opam b/opam
index e4f80be..d25fc9d 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/iris-c" ]
 depends: [
-  "coq-iris" { (= "dev.2020-10-13.1.5558d66d") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
 ]
diff --git a/theories/lib/flock.v b/theories/lib/flock.v
index 22fdd40..f6148dd 100644
--- a/theories/lib/flock.v
+++ b/theories/lib/flock.v
@@ -345,8 +345,7 @@ Section flock.
         symmetry in Heqfaρ.
         iCombine "Hactives Hρ" as "H".
         iDestruct (own_valid with "H") as %Hbaz.
-        exfalso. apply auth_frag_valid in Hbaz. simpl in *.
-        specialize (Hbaz ρ). revert Hbaz.
+        exfalso. move: Hbaz. rewrite auth_frag_valid=> /(_ ρ).
         rewrite lookup_op Heqfaρ lookup_singleton.
         rewrite -Some_op Some_valid.
         eapply exclusive_r ; eauto. apply _. }
-- 
GitLab