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

---
 opam                            |  2 +-
 theories/examples/ticket_lock.v |  4 ++--
 theories/logic/spec_ra.v        | 10 ++++------
 3 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/opam b/opam
index 46637ba..098d46a 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-10-15.2.f4060bb5") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 83aa92c..dc46d11 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -46,8 +46,8 @@ Section refinement.
 
   Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
   Proof.
-    iIntros "Ht1 Ht2".
-    iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
+    iIntros "Ht1 Ht2". iDestruct (own_valid_2 with "Ht1 Ht2")
+      as %?%auth_frag_op_valid_1%gset_disj_valid_op.
     set_solver.
   Qed.
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 5e76800..54c7ace 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -165,12 +165,10 @@ Section mapsto.
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply bi.wand_intro_r.
-    rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
-    f_equiv=> /=.
-    rewrite -pair_op singleton_op right_id -pair_op.
-    move=> [_ Hv]. move:Hv => /=.
-    rewrite singleton_valid.
-    by move=> [_] /to_agree_op_inv_L [->].
+    rewrite heapS_mapsto_eq -own_op own_valid uPred.discrete_valid. f_equiv.
+    rewrite auth_frag_op_valid -pair_op singleton_op -pair_op.
+    rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L.
+    by intros [_ [_ [=]]].
   Qed.
 
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
-- 
GitLab