diff --git a/opam b/opam
index ec4e7bc8ee89ee4a77c11ecb371ff376b9c473be..e8fe5ce51fc33013bb5840ec77356ac01e34553f 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-12.4.ae1dd418") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logrel/F_mu/soundness.v b/theories/logrel/F_mu/soundness.v
index ade3e7d015244840d2b11f45d4ca04c7ddc07473..ce7b3fbe6ce9bf0a8663770c12c765ad215f8136 100644
--- a/theories/logrel/F_mu/soundness.v
+++ b/theories/logrel/F_mu/soundness.v
@@ -9,7 +9,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
 Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ); eauto.
-  iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I). iSplit=> //.
+  iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //.
   replace e with e.[env_subst[]] by by asimpl.
   set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
diff --git a/theories/logrel/F_mu_ref/soundness.v b/theories/logrel/F_mu_ref/soundness.v
index f75f2312c47970d3f6ee8c85c281db4e94f2ab37..fff5f5a440b7dc3b447c2c91d21598ba2456d2c4 100644
--- a/theories/logrel/F_mu_ref/soundness.v
+++ b/theories/logrel/F_mu_ref/soundness.v
@@ -17,7 +17,7 @@ Proof.
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
   iMod (gen_heap_init σ) as (Hheap) "Hh".
-  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   set (HeapΣ := (HeapG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
diff --git a/theories/logrel/F_mu_ref/soundness_binary.v b/theories/logrel/F_mu_ref/soundness_binary.v
index 00bbf0c8f2e08efacdf50e39c937615866a9593c..b16a847278e2c616c034136c27d55e8c3bf3bd2b 100644
--- a/theories/logrel/F_mu_ref/soundness_binary.v
+++ b/theories/logrel/F_mu_ref/soundness_binary.v
@@ -25,7 +25,7 @@ Proof.
     rewrite /to_gen_heap fin_maps.map_fmap_empty.
     iFrame. }
   set (HeapΣ := HeapG Σ Hinv Hheap).
-  iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   iApply wp_fupd. iApply (wp_wand with "[-]").
   - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
     { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index bf10c67126d424921d277bd7b701e2a9ca4f731a..d747ae174d19922d61ebf5f07bdd46297cdfb8e4 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -22,7 +22,7 @@ Proof.
   iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], ∅. rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
   set (HeapΣ := (HeapIG Σ Hinv Hheap)).
-  iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   iApply wp_fupd. iApply wp_wand_r.
   iSplitL.
   iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
diff --git a/theories/logrel/F_mu_ref_conc/soundness_unary.v b/theories/logrel/F_mu_ref_conc/soundness_unary.v
index 7a1213f2bcb096c6e509add2c727acb6cb0e3db0..c122efada7b864d04ce244740b0a79ffe2636135 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_unary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_unary.v
@@ -16,7 +16,7 @@ Proof.
   intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
   iMod (gen_heap_init σ) as (Hheap) "Hh".
-  iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame.
+  iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
   set (HeapΣ := (HeapIG Σ Hinv Hheap)).
   iApply (wp_wand with "[]").
   - replace e with e.[env_subst[]] by by asimpl.
diff --git a/theories/logrel/stlc/soundness.v b/theories/logrel/stlc/soundness.v
index be359de05dbb77fcaf05f8277ec3d2886fed6fdc..d080562e292be4019a2664a4473588a9da91a477 100644
--- a/theories/logrel/stlc/soundness.v
+++ b/theories/logrel/stlc/soundness.v
@@ -16,7 +16,7 @@ Proof.
   set (Σ := invΣ). intros.
   cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto).
   eapply (wp_adequacy Σ _). iIntros (Hinv ?).
-  iModIntro. iExists (λ _ _, True%I). iSplit=>//.
+  iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//.
   set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
 Qed.