From bcfa9d23d6d983b31b89ac69b7409df1d3dc510e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 May 2020 10:35:50 +0200
Subject: [PATCH] Bump Iris (sbi removal).

---
 opam                                            | 2 +-
 theories/barrier/example_joining_existentials.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index cd2f051..89775aa 100644
--- a/opam
+++ b/opam
@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
 synopsis: "A collection of case studies for Iris"
 
 depends: [
-  "coq-iris" { (= "dev.2020-05-18.2.fdda97e8") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
   "coq-iris-string-ident"
 ]
diff --git a/theories/barrier/example_joining_existentials.v b/theories/barrier/example_joining_existentials.v
index 1022739..4498692 100644
--- a/theories/barrier/example_joining_existentials.v
+++ b/theories/barrier/example_joining_existentials.v
@@ -58,7 +58,7 @@ Proof.
   iDestruct 1 as (x) "[#Hγ Hx]"; iDestruct 1 as (x') "[#Hγ' Hx']".
   iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
-    rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
+    rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
     rewrite -{2}[x]oFunctor_map_id -{2}[x']oFunctor_map_id.
     assert (HF : oFunctor_map F (cid, cid) ≡ oFunctor_map F (iProp_fold (Σ:=Σ) ◎
         iProp_unfold, iProp_fold (Σ:=Σ) ◎ iProp_unfold)).
-- 
GitLab