update dependencies; fix for mapsto_malid_2 changes

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" }
 ]

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].

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.

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.

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.