diff --git a/opam b/opam
index 6ec89d7e1785da3d8d515e651b5a86e28bdf5da2..b04df149f81906206b06bfb05b02dfb116783090 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-02-15.5") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-02-21.8") | (= "dev") }
 ]
diff --git a/theories/fractor.v b/theories/fractor.v
index 37b9d1813470f06f363bcff209dc1982a84b98ba..8edd8397c45b4e87ed400e0dbdeb7ea88e8b8a9f 100644
--- a/theories/fractor.v
+++ b/theories/fractor.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth frac excl gmap .
 From iris.bi Require Import big_op fractional.
 From iris.base_logic.lib Require Import cancelable_invariants.
+From stdpp Require Export namespaces.
 
 Import uPred.
 
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index ff160d850b357490646e6bb8720b5cd3c48e8b6c..a3ff8cd6242ec52eb0e12855a57d52d41b272f2a 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import weakestpre. (* TODO: why ??? *)
 From igps.gps Require Export inst_shared.
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index 5fabc4652a71d9e40f86796ba6f5b2c47a28a54d..e1b73905615a84fed91897c94d27a1e6386c51d8 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import weakestpre. (* TODO: why ??? *)
 From igps.gps Require Export inst_shared.
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index 3ba264c4f7cc4b3bcd5e01f757d5826b3012c775..4241635b225e2c9c5c61f83fa76bbfccae0e2449 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -1,4 +1,4 @@
-From iris.base_logic Require Import iprop namespaces lib.cancelable_invariants.
+From iris.base_logic Require Import iprop lib.cancelable_invariants.
 From iris.proofmode Require Import tactics.
 From igps.gps Require Export inst_shared.
 From igps Require Import bigop.
diff --git a/theories/logically_atomic.v b/theories/logically_atomic.v
index d05b9532d422f393fd1566c35ac494a6662f7d28..7961c732c5dd943e753dc4ed66ef10d768ae3993 100644
--- a/theories/logically_atomic.v
+++ b/theories/logically_atomic.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.base_logic Require Import iprop namespaces.
+From iris.base_logic Require Import iprop.
 From iris.program_logic Require Import ownp.
 From igps Require Import ghosts weakestpre invariants. (* TODO: why ??? *)
 Import base.
diff --git a/theories/rsl.v b/theories/rsl.v
index 89a49b8df0e261077fd93c27bf66ea6024414e0e..802845a5c04ade0a6d640bc4691ba19fb945cf7d 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -934,8 +934,8 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
       iSplitR ""; last iSplitL "".
       + rewrite /RSLInv /sts_inv.
         iExists j, γ. iModIntro. iSplitL ""; first by iNext.
-        iExists s'. iFrame "Own Hist' ress2".
-        iNext. iSplit; first auto. iNext. iSplitR "ressD"; last first.
+        iExists s'. rewrite /rsl_inv /s'. iFrame "Own Hist'". iSplit; first auto.
+        iSplitR "ressD ress2"; [|iSplitR "ress2"; [|done]]; last first; iNext; iNext.
         * iApply (big_sepS_subseteq _ _ h' with "[$ressD]").
           by rewrite H11 union_comm_L.
         * iApply (big_sepS_subseteq _ _ (gblock_ends l h') with "[$ress]").
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 6f00bcf0e8683745f8accd40b7037123a7dc2f8b..22e05c2fc92f1e6b44d4b5eb6c6c934f21d6345e 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -8,7 +8,7 @@ Import uPred.
 Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec (Λ:=ra_lang) φ e1 e2 →
   φ →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
   envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 9d2c54176c798e55dd5f6e7b913e66f521773c3a..5d0640c7a64542fcc9b90fbdc3c9ad9e5b1c42e2 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -19,7 +19,7 @@ Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
   (PureExec (Λ:=surface_lang) φ (e1) (e2)) →
   φ →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP e2 @ E {{ Φ }}) →
   envs_entails Δ (WP e1 @ E {{ Φ }}).
 Proof.