diff --git a/opam b/opam
index e8fe5ce51fc33013bb5840ec77356ac01e34553f..a26355d0974d3fd3fe588ccd6da438dcff5f2732 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-12.4.ae1dd418") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/logrel/stlc/soundness.v b/theories/logrel/stlc/soundness.v
index d080562e292be4019a2664a4473588a9da91a477..3c50d7e15567850732853a5997bf7be0a59b8933 100644
--- a/theories/logrel/stlc/soundness.v
+++ b/theories/logrel/stlc/soundness.v
@@ -20,4 +20,3 @@ Proof.
   set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
   iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
 Qed.
-