Bump Iris.

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

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)

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 = ∅⌝.