diff --git a/opam b/opam
index 769e5c305f8fd0bcac9a3af63f9b37ea29bc318a..c5a7746a29142befd3c565dbc8e54975d73bec5b 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" { (= "dev.2018-10-04.7.fc21b664") | (= "dev") }
+  "coq-iris" { (= "dev.2018-10-05.4.464c2449") | (= "dev") }
 ]
diff --git a/theories/lifting.v b/theories/lifting.v
index 650dd0cb41254487fbf9cf0826c6695a24849027..915248ccccf92c30ba38b4df518a77aebd911329 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -951,7 +951,8 @@ Local Ltac solve_pure_exec :=
   repeat match goal with H : IntoVal (_,_) (_,_) |- _ =>
                    rewrite /IntoVal /= /of_val in H; revert H; intros [= ?] end;
   repeat match goal with H : AsVal (_,_) |- _ => destruct H as [[??] [= ??]] end;
-  subst; apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
+  constructor; [ solve_exec_safe | solve_exec_puredet ].
 
 Class AsRec (e : base.expr) (f x : base.binder) (erec : base.expr) :=
   as_rec : e = base.Rec f x erec.
@@ -962,27 +963,27 @@ Proof. by unlock. Qed.
 
 Global Instance pure_rec f x (erec e1 e2 : base.expr) V
        `{!AsVal (e2,V), AsRec e1 f x erec, base.Closed (f :b: x :b: []) erec}:
-  PureExec True (base.App e1 e2, V) (base.subst' x e2 (base.subst' f e1 erec), V).
+  PureExec True 1 (base.App e1 e2, V) (base.subst' x e2 (base.subst' f e1 erec), V).
 Proof.
   intros. unfold AsRec in *. solve_pure_exec.
 Qed.
 
 Global Instance pure_unop op e v v' V `{!IntoVal (e,V) (v,V)}:
-  PureExec (base.un_op_eval op v = Some v') (base.UnOp op e, V) (base.of_val v', V).
+  PureExec (base.un_op_eval op v = Some v') 1 (base.UnOp op e, V) (base.of_val v', V).
 Proof.
   intros. solve_pure_exec.
 Qed.
 
 Global Instance pure_binop op e1 e2 v1 v2 v' V `{!IntoVal (e1,V) (v1,V), !IntoVal (e2,V) (v2,V)}:
-  PureExec (base.bin_op_eval op v1 v2 = Some v') (base.BinOp op e1 e2, V) (base.of_val v',V).
+  PureExec (base.bin_op_eval op v1 v2 = Some v') 1 (base.BinOp op e1 e2, V) (base.of_val v',V).
 Proof.
   intros. solve_pure_exec.
 Qed.
 
 Global Instance pure_if_true e1 e2:
-  ∀ V, PureExec True (base.If (base.Lit (base.LitInt 1)) e1 e2, V) (e1, V).
+  ∀ V, PureExec True 1 (base.If (base.Lit (base.LitInt 1)) e1 e2, V) (e1, V).
 Proof. intros. solve_pure_exec. Qed.
 
 Global Instance pure_if_false e1 e2:
-  ∀ V, PureExec True (base.If (base.Lit (base.LitInt 0)) e1 e2, V) (e2, V).
+  ∀ V, PureExec True 1 (base.If (base.Lit (base.LitInt 0)) e1 e2, V) (e2, V).
 Proof. intros. solve_pure_exec. Qed.
diff --git a/theories/lifting_vProp.v b/theories/lifting_vProp.v
index 288af7c8ddd943dac168ce1d5d33d0dbe0672440..b6a1e1b4b68f8eb3d258a6eadead25d459a12d6d 100644
--- a/theories/lifting_vProp.v
+++ b/theories/lifting_vProp.v
@@ -3,20 +3,23 @@ From iris.program_logic Require Import language.
 From igps Require Import lang.surface viewpred weakestpre proofmode.
 Export lang.base lang.surface.
 
-Lemma pure_exec_view Φ (e1 e2 : base.expr) :
-  PureExec Φ e1 e2 → ∀ V, PureExec (Λ:=ra_lang) Φ (e1, V) (e2, V).
+Lemma pure_exec_view Φ n (e1 e2 : base.expr) :
+  PureExec Φ n e1 e2 → ∀ V, PureExec (Λ:=ra_lang) Φ n (e1, V) (e2, V).
 Proof.
-  intros PE.
+  intros PE V HΦ. specialize (PE HΦ). clear HΦ Φ. revert V.
+  induction PE as [|???? PE _ IH].
+  { intros. constructor. }
+  intros V. econstructor; last exact: IH. clear IH.
   inversion PE; intros; econstructor.
-  - intros σ HΦ. move: pure_exec_safe => /(_ (V,σ) HΦ); intros (e' & [V' σ'] & efs & HStep).
+  - intros σ. move: pure_step_safe => /(_ (V,σ)); intros (e' & [V' σ'] & efs & HStep).
     exists (e',V'), σ', (map (fun e => (e,V')) efs).
     inversion HStep.
     exists K (e1', V) (e2', V').
     + simplify_eq. now rewrite -fill_view.
     + simplify_eq. now rewrite -fill_view.
     + now eauto.
-  - intros σ1 [e2' V'] σ2 efs HΦ HStep.
-    move: pure_exec_puredet => /(_ (V, σ1) e2' (V', σ2) (map (fst) efs) HΦ) H.
+  - intros σ1 [e2' V'] σ2 efs HStep.
+    move: pure_step_det => /(_ (V, σ1) e2' (V', σ2) (map (fst) efs)) H.
     destruct H as (? & ? & ?).
     + inversion HStep; cbn in *.
       destruct e1' as [e1' V1'], e2'0 as [e2'0 V2'0]. cbn in *.
@@ -41,7 +44,7 @@ Implicit Types P Q : vProp Σ.
 Implicit Types Φ : base.val → vProp Σ. (* TODO: fix imports *)
 
 Lemma wp_pure_step_later `{Inhabited (state)} E e1 e2 φ Φ :
-  (PureExec φ e1 e2) →
+  (PureExec φ 1 e1 e2) →
   φ →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
 Proof.
@@ -95,25 +98,26 @@ Local Ltac solve_exec_puredet := simpl; intros; inv_head_step;
 Local Ltac solve_pure_exec :=
   unfold IntoVal,AsRec in *; subst;
   repeat match goal with H : AsVal _ |- _ => destruct H as [??] end;
-  apply ectx_language.det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+  intros ?; apply nsteps_once, ectx_language.pure_head_step_pure_step;
+  constructor; [ solve_exec_safe | solve_exec_puredet ].
 
 Global Instance pure_rec f x (erec e1 e2 : base.expr)
        `{!AsVal (e2), AsRec e1 f x erec, base.Closed (f :b: x :b: []) erec}:
-  PureExec True (base.App e1 e2) (base.subst' x e2 (base.subst' f e1 erec)).
+  PureExec True 1 (base.App e1 e2) (base.subst' x e2 (base.subst' f e1 erec)).
 Proof. solve_pure_exec. Qed.
 
 Global Instance pure_unop op e v v' `{!IntoVal (e) (v)}:
-  PureExec (base.un_op_eval op v = Some v') (base.UnOp op e) (base.of_val v').
+  PureExec (base.un_op_eval op v = Some v') 1 (base.UnOp op e) (base.of_val v').
 Proof. solve_pure_exec. Qed.
 
 Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal (e1) (v1), !IntoVal (e2) (v2)}:
-  PureExec (base.bin_op_eval op v1 v2 = Some v') (base.BinOp op e1 e2) (base.of_val v').
+  PureExec (base.bin_op_eval op v1 v2 = Some v') 1 (base.BinOp op e1 e2) (base.of_val v').
 Proof. solve_pure_exec. Qed.
 
 Global Instance pure_if_true e1 e2:
-  PureExec True (base.If (base.Lit (base.LitInt 1)) e1 e2) (e1).
+  PureExec True 1 (base.If (base.Lit (base.LitInt 1)) e1 e2) (e1).
 Proof. solve_pure_exec. Qed.
 
 Global Instance pure_if_false e1 e2:
-  PureExec True (base.If (base.Lit (base.LitInt 0)) e1 e2) (e2).
+  PureExec True 1 (base.If (base.Lit (base.LitInt 0)) e1 e2) (e2).
 Proof. intros. solve_pure_exec. Qed.
diff --git a/theories/wp_tactics.v b/theories/wp_tactics.v
index 4d981a488fd8b076d3699242375206a021d90f77..91f80b533c0bbc2ef4ae7f2e217a1645c54812f2 100644
--- a/theories/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -6,7 +6,7 @@ From igps Require Export lifting tactics_vProp ghosts.
 Import uPred.
 
 Lemma tac_wp_pure `{ghosts.foundationG Σ} K Δ Δ' E e1 e2 φ Φ :
-  PureExec (Λ:=ra_lang) φ e1 e2 →
+  PureExec (Λ:=ra_lang) φ 1 e1 e2 →
   φ →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 93659610906fc1b4dc282c8527afed8f26d8ee62..96b7d21790bc32e3e2befce06aa96407e9ac762f 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -17,7 +17,7 @@ Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
 Lemma tac_wp_pure `{foundationG Σ} Δ Δ' E e1 e2 φ Φ :
-  (PureExec (Λ:=surface_lang) φ (e1) (e2)) →
+  (PureExec (Λ:=surface_lang) φ 1 (e1) (e2)) →
   φ →
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP e2 @ E {{ Φ }}) →
@@ -41,7 +41,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     unify e' efoc;
     eapply tac_wp_pure;
     [
-      simple apply (language.pure_exec_ctx _ (H:=ectx_language.ectx_lang_ctx (Λ:=surface_ectx_lang) K) e' _ _ _) (* FIXME *)
+      refine (@language.pure_exec_ctx _ _ (ectx_language.ectx_lang_ctx (Λ:=surface_ectx_lang) K) _ _ e' _ _); apply _ (* FIXME *)
                                     (* PureExec *)
     |try fast_done                  (* The pure condition for PureExec *)
     |apply _                        (* IntoLaters *)