diff --git a/opam b/opam
index 9327471f167a710a7a51d2a659aae314c4fb2a7d..639056c099280d9361896f94c278ddc98f8d7e19 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-06-14.8.bf9fd4f5") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-06-15.3.d88d654b") | (= "dev") }
 ]
diff --git a/theories/adequacy.v b/theories/adequacy.v
index a5ef9c8f1375b60ea56087ee8ab8195c72bd58ae..5308ce4c0005c05b6aeb4b0eecf58bd4cb29f7f3 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -222,7 +222,7 @@ Proof.
     iCombine "A" "B" as "AB".
     rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM.
     match goal with
-    | |- coq_tactics.envs_entails _ (big_opM _ ?f ?g) =>
+    | |- environments.envs_entails _ (big_opM _ ?f ?g) =>
       iApply (big_sepM_impl _ f with "[$AB]")
     end.
     iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0.