diff --git a/opam b/opam
index 098d46ae23cea90933ae57bb073cfea2b202e6c5..61344afd08ae5cdb389cdca9fd1243d32a0c0724 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 494c19608567519be9433bddde7ebb8542511814..890d79c84f7d7073c379306d226125f966b16237 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 fbbf5d719133c5b13457e2dcaaded8b30efe6cfc..afae6758d6552d0458434f0500431cca1adf722a 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 2bb656743ce858876c2b27857fcb89dc58a5a566..0f86864ba99b3342e713c09c120bfae0a7eea185 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 1b4e4b566d1afde5e8a8d4e53cc10df3ac2e5151..728f5546853ee0fee16bbecda9dda38cf0b8be15 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.