From da7951b4c0cd1e73d9785de895da7e5fa1b7a690 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Jul 2020 12:36:43 +0200
Subject: [PATCH] Bump Iris.

---
 opam                                          | 2 +-
 theories/experimental/helping/helping_stack.v | 2 +-
 theories/typing/interp.v                      | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index 5048e10..223fd05 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 be39de8..42121a7 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 a87c103..3f6e230 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 = ∅⌝.
-- 
GitLab