From 414d0dfadc5ab074bc157c1231210af42c975bbc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Nov 2020 16:56:03 +0100
Subject: [PATCH] update dependencies; fix for mapsto_malid_2 changes

---
 opam                                   | 2 +-
 theories/examples/namegen.v            | 2 +-
 theories/examples/various.v            | 4 ++--
 theories/experimental/helping/offers.v | 2 +-
 theories/logic/model.v                 | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/opam b/opam
index 098d46a..61344af 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-20.2.c65b38ea") | (= "dev") }
+  "coq-iris" { (= "dev.2020-11-03.2.231ab52f") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 494c196..890d79c 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -64,7 +64,7 @@ Section namegen_refinement.
       { iIntros (Hy). destruct Hy as [y Hy].
         rewrite (big_sepS_elem_of _ L (l',y) Hy).
         iDestruct "HL" as "[Hl _]".
-        iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+        iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
         compute in Hfoo. eauto. }
       iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc.
       { iIntros (Hx). destruct Hx as [x Hy].
diff --git a/theories/examples/various.v b/theories/examples/various.v
index fbbf5d7..afae675 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -232,7 +232,7 @@ Section proofs.
         iDestruct "Hx'" as "[Hx' Hx'1]".
         iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
         { iCombine "Hx Hx1" as "Hx".
-          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
           compute in Hfoo. eauto. }
         iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
         { iNext. iExists (S n).
@@ -244,7 +244,7 @@ Section proofs.
         iDestruct (mapsto_agree with "Hx Hx1") as %->.
         iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
         { iCombine "Hx Hx1" as "Hx".
-          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
           compute in Hfoo. eauto. }
         iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
         rel_store_r.
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index 2bb6567..0f86864 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -37,7 +37,7 @@ Section rules.
     is_offer γ1 l P1 Q1 -∗ is_offer γ2 l P2 Q2 -∗ False.
   Proof.
     iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
-    iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %?. contradiction.
+    iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[??]. contradiction.
   Qed.
 
   Lemma make_is_offer γ l P Q : l ↦ #0 -∗ P -∗ is_offer γ l P Q.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 1b4e4b5..728f554 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -170,7 +170,7 @@ Section semtypes_properties.
     iInv (relocN.@"ref".@(l, l1')) as (? ?) "[>Hl ?]" "Hcl".
     iInv (relocN.@"ref".@(l, l2')) as (? ?) "[>Hl' ?]" "Hcl'".
     simpl. iExFalso.
-    iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+    iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
     compute in Hfoo. eauto.
   Qed.
 
-- 
GitLab