From 99d3d681d85ed36e57ec07f6e2ae5cb9bf3f9590 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Sep 2020 09:02:34 +0200
Subject: [PATCH] update dependencies, fix for agree_op_inv rename

---
 opam                                  | 2 +-
 theories/experimental/hocap/counter.v | 2 +-
 theories/logic/spec_ra.v              | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index e4bec29..cbd9717 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-09-03.0.96df7997") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-14.5.5d04e9aa") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 0b9ea42..85e3733 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -71,7 +71,7 @@ Section cnt_model.
     iPureIntro. revert Hfoo.
     rewrite -auth_frag_op -Some_op -pair_op.
     rewrite auth_frag_valid Some_valid.
-    by intros [_ foo%agree_op_invL']%pair_valid.
+    by intros [_ foo%to_agree_op_inv_L']%pair_valid.
   Qed.
 
   Lemma cnt_agree_2 γ q n m :
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 90dcc44..567e3b7 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -142,7 +142,7 @@ Section mapsto.
     rewrite -pair_op singleton_op right_id -pair_op.
     move=> [_ Hv]. move:Hv => /=.
     rewrite singleton_valid.
-    by move=> [_] /agree_op_invL' [->].
+    by move=> [_] /to_agree_op_inv_L' [->].
   Qed.
 
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
-- 
GitLab