diff --git a/opam b/opam
index 5048e109ec5f34b94481d0fac2500a70a7b781ad..223fd052a4737373fc320e3f3211c0a9b6713f0d 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-06-18.3.5f98a0bf") | (= "dev") }
+  "coq-iris" { (= "dev.2020-07-02.0.59a1ad49") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index be39de80d5ada418fd3877b1b33a09551e9c6aef..42121a71fd50808ffc39c9cf1b45f48a2151573e 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -252,7 +252,7 @@ Section refinement.
       This is also the only place where we need to unfold the definition of the refinement proposition. *)
   Lemma revoke_offer_l γ off E K (v : val) e1 e2 A :
     offer_token γ -∗
-    (∀ j K', (j ⤇ fill K' e1)  ={E, ⊤, E}▷=∗
+    (∀ j K', (j ⤇ fill K' e1)  ={E}[⊤]▷=∗
       ▷ is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) ∗
       ▷ (is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) -∗
            ((REL fill K (of_val NONEV) << e2 @ E : A)
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index a87c103b4973da8cc159b9774905ca8c7eebdced..3f6e230b48e8f31a45c724174cb5c5ad3add8dc1 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -213,7 +213,7 @@ Section env_typed.
 
   Lemma env_ltyped2_empty :
     ⊢ ⟦ ∅ ⟧* ∅.
-  Proof. apply big_sepM2_empty'. Qed.
+  Proof. apply (big_sepM2_empty' _). Qed.
 
   Lemma env_ltyped2_empty_inv vs :
     ⟦ ∅ ⟧* vs -∗ ⌜vs = ∅⌝.