diff --git a/opam b/opam
index 94e2144e5685fb3a90093283891e77775b061dec..32a6c2a37b2987e569b24bf995a7cea05ab867a2 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2018-02-20.1") | (= "dev") }
+  "coq-iris" { (= "dev.2018-02-21.1") | (= "dev") }
 ]
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index ecf05a0287ec6003686851ec868f8dccd14f9f0b..7ec0166ce28eec7884dc2831e8675c34423b7875 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
 Set Default Proof Using "Type".
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 35f9503727d13f1854ee4afd307b83cead02d191..2320c69c5734d9db57d88617fed96f9c8864ed1d 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode memcpy.
 Set Default Proof Using "Type".
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 38d96b17f28d1a06de83a70cac958db553cb34e0..86bd32061c0ef671bba2bda04b3042ddd2008b2a 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import heap proofmode.
 Set Default Proof Using "Type".
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index da0a116e317d1f2e11d2a219233267fd8ee2d805..9c7eb8132f905a61f97aa3350169011b0cd54d96 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.