From 00c7f96e1d6d996418d347bd6c8fb40294b2c86e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Sep 2020 10:34:50 +0200
Subject: [PATCH] update dependencies; fix for agree_op rename

---
 opam                              | 2 +-
 theories/logrel/examples/double.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index aad382c..4f214a0 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-09-03.1.7dd1b9af") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-15.3.986a8883") | (= "dev") }
 ]
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 7bf2260..1bf7523 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -113,10 +113,10 @@ Section double.
     - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
       + by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
       + iDestruct "H2" as (v2') "(_&H1'&HP)".
-        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%agree_op_invL'].
+        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%to_agree_op_inv_L].
         iApply "HΦ"; auto.
       + iDestruct "H1" as (v1') "(_&H2'&HP)".
-        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%agree_op_invL'].
+        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%to_agree_op_inv_L].
         iApply "HΦ"; auto.
       + iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
         by iDestruct (own_valid_2 with "H1 H2") as %[].
-- 
GitLab