diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1f76dc8c99744405082ba86867f64110833fce1e..0bc57c96f3a0ef5de51bb7580fbe7f29f851f004 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -33,6 +33,11 @@ build-coq.dev:
     OPAM_PINS: "coq version dev"
     VALIDATE: "1"
 
+build-coq.8.8.2:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.8.2"
+
 build-coq.8.8.1:
   <<: *template
   variables:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1ba5406386774c980ac17abcc7c31feda1152b6..6212f09f39d6119895d6284dc61b88630d0650d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,7 +29,7 @@ Changes in and extensions of the theory:
   functions.
 * [#] Add atomic updates and logically atomic triples, including tactic support.
   See `heap_lang/lib/increment.v` for an example.
-* [#] HeapLang now uses right-to-left evaluation order. This makes it
+* [#] heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.
 
 Changes in Coq:
@@ -84,6 +84,7 @@ Changes in Coq:
 * Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
   changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 * `wp_fork` is now written in curried form.
+* `PureExec`/`wp_pure` now supports taking multiple steps at once.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
diff --git a/README.md b/README.md
index a96743610ca7341f9a097c41c98594ac11fd542e..02359e0b74d33fbb2cb805ba9efd45d79bcf6c7e 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
 
 This version is known to compile with:
 
- - Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1
+ - Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
  - A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
 
 For a version compatible with Coq 8.6, have a look at the
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index f924a6f9b4a9b059759b34027b51d3b0038fbe9f..8b7b2753697918f72071b9827a690aa73465484f 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -962,16 +962,6 @@ Section persistently_affine_bi.
       rewrite assoc -persistently_and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
-  Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
-  Proof.
-    apply (anti_symm (⊢)).
-    - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
-      apply and_mono_r. rewrite -persistently_pure.
-      apply persistently_intro', wand_intro_l.
-      by rewrite impl_elim_r persistently_pure right_id.
-    - apply exist_elim=> R. apply impl_intro_l.
-      by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
-  Qed.
 End persistently_affine_bi.
 
 (* The intuitionistic modality *)
@@ -1082,6 +1072,16 @@ Proof.
     apply sep_mono; first done. apply and_elim_r.
 Qed.
 
+Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
+    apply and_mono_r. rewrite impl_elim_r -entails_wand //.
+    apply persistently_emp_intro.
+  - apply exist_elim=> R. apply impl_intro_l.
+    rewrite assoc persistently_and_intuitionistically_sep_r.
+    by rewrite intuitionistically_elim wand_elim_r.
+Qed.
 
 Section bi_affine_intuitionistically.
   Context `{BiAffine PROP}.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 3bccac51bfd306bfc5d7c2fc7c17e756376c3f74..56bda4ca51c97bab21f2a5f738005a33e3a8e63a 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
   for this is that it makes curried functions usable: Given a WP for [f a b], we
   know that any effects [f] might have to not matter until after *both* [a] and
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
-  useless the user let-expands [b].
+  useless unless the user let-expands [b].
 
 - For prophecy variables, we annotate the reduction steps with an "observation"
   and tweak adequacy such that WP knows all future observations.  There is
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 7d701ae819daa8959453963755ed7e509b71f231..3eae9130293a85349e87fbe210105df833d94373 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -64,7 +64,8 @@ Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
   unfold IntoVal in *;
   repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
-  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+  intros ?; apply nsteps_once, pure_head_step_pure_step;
+    constructor; [solve_exec_safe | solve_exec_puredet].
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
   as_rec : e = Rec f x erec.
@@ -75,37 +76,37 @@ Proof. by unlock. Qed.
 
 Instance pure_rec f x (erec e1 e2 : expr)
     `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
-  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
+  PureExec True 1 (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
 Instance pure_unop op e v v' `{!IntoVal e v} :
-  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
+  PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (of_val v').
 Proof. solve_pure_exec. Qed.
 
 Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
-  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
+  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True 1 (If (Lit (LitBool true)) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True 1 (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
-  PureExec True (Fst (Pair e1 e2)) e1.
+  PureExec True 1 (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
-  PureExec True (Snd (Pair e1 e2)) e2.
+  PureExec True 1 (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
+  PureExec True 1 (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
-  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
+  PureExec True 1 (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pure_exec. Qed.
 
 Section lifting.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index b94a1a5db3184ee34dec96e02078a8d7d502d87b..c165adbceebfc5a0dc6686a523e6e169aa57a138 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -115,18 +115,17 @@ Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
 (* When parsing lambdas, we want them to be locked (so as to avoid needless
 unfolding by tactics and unification). However, unlocked lambda-values sometimes
 appear as part of compound expressions, in which case we want them to be pretty
-printed too. We achieve that by first defining the non-locked notation, and then
-the locked notation. Both will be used for pretty-printing, but only the last
-will be used for parsing. *)
+printed too. We achieve that by using printing only notations for the non-locked
+notation. *)
 Notation "λ: x , e" := (LamV x%bind e%E)
   (at level 200, x at level 1, e at level 200,
-   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+   format "'[' 'λ:'  x ,  '/  ' e ']'", only printing) : val_scope.
 Notation "λ: x , e" := (locked (LamV x%bind e%E))
   (at level 200, x at level 1, e at level 200,
    format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
 Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
   (at level 200, x, y, z at level 1, e at level 200,
-   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'", only printing) : val_scope.
 Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index e2324fd403309de1cc3c35b452bb0fdd9f2d83ba..979c7773d5ba82c088ce24c1edc730bea7592a6a 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -30,18 +30,18 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
-Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs n Δ Δ' →
   envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
   envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
   envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
   envs_entails Δ (WP e1 @ s; E [{ Φ }]).
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index c767b8115465f4255c2a74269b22b0832f2625c4..45eaf1cc1bc02219bf9cde8ef9cce82028e9f972 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -214,23 +214,24 @@ Section ectx_language.
       econstructor; eauto.
   Qed.
 
-  Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
-    (∀ σ, P → head_reducible_no_obs e1 σ) →
-    (∀ σ1 κ e2' σ2 efs,
-      P → head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
-    PureExec P e1 e2.
+  Record pure_head_step (e1 e2 : expr Λ) := {
+    pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
+    pure_head_step_det σ1 κ e2' σ2 efs :
+      head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
+  }.
+
+  Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 → pure_step e1 e2.
   Proof.
-    intros Hp1 Hp2. split.
-    - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
+    intros [Hp1 Hp2]. split.
+    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
       eexists e2', σ2, efs. by apply head_prim_step.
-    - intros σ1 κ e2' σ2 efs ? ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
+    - intros σ1 κ e2' σ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
   Qed.
 
-  Global Instance pure_exec_fill K e1 e2 φ :
-    PureExec φ e1 e2 →
-    PureExec φ (fill K e1) (fill K e2).
+  Global Instance pure_exec_fill K φ n e1 e2 :
+    PureExec φ n e1 e2 →
+    PureExec φ n (fill K e1) (fill K e2).
   Proof. apply: pure_exec_ctx. Qed.
-
 End ectx_language.
 
 Arguments ectx_lang : clear implicits.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 102c381fce69b6cb81fe38642226738f0459eb0f..969eb63bfd372cb952629e1b5bdb57fbcd2237a2 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -177,31 +177,40 @@ Section language.
     intros* Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
   Qed.
 
-  Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
-    pure_exec_safe σ :
-      P → reducible_no_obs e1 σ;
-    pure_exec_puredet σ1 κ e2' σ2 efs :
-      P → prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
+  Record pure_step (e1 e2 : expr Λ) := {
+    pure_step_safe σ1 : reducible_no_obs e1 σ1;
+    pure_step_det σ1 κ e2' σ2 efs :
+      prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
   }.
 
-  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
-    (P → PureExec True e1 e2) →
-    PureExec P e1 e2.
-  Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
+  (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
+  succeeding when it did not actually do anything. *)
+  Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
+    pure_exec : φ → relations.nsteps pure_step n e1 e2.
 
-  (* We do not make this an instance because it is awfully general. *)
-  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
-    PureExec φ e1 e2 →
-    PureExec φ (K e1) (K e2).
+  Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
+    pure_step e1 e2 →
+    pure_step (K e1) (K e2).
   Proof.
     intros [Hred Hstep]. split.
     - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
-    - intros σ1 κ e2' σ2 efs ? Hpstep.
+    - intros σ1 κ e2' σ2 efs Hpstep.
       destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
       + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
       + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 
+  Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
+    relations.nsteps pure_step n e1 e2 →
+    relations.nsteps pure_step n (K e1) (K e2).
+  Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
+
+  (* We do not make this an instance because it is awfully general. *)
+  Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
+    PureExec φ n e1 e2 →
+    PureExec φ n (K e1) (K e2).
+  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
+
   (* This is a family of frequent assumptions for PureExec *)
   Class IntoVal (e : expr Λ) (v : val Λ) :=
     into_val : of_val v = e.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 42d4b72727392a89931dfd3c976f6bb2efcb430c..5b836d2bf1b384941ea4924fd402bad07bb3b19a 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -127,23 +127,25 @@ Proof.
   by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  Nat.iter n (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros ([??] Hφ) "HWP".
-  iApply (wp_lift_pure_det_step with "[HWP]").
-  - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
+  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iApply wp_lift_pure_det_step.
+  - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
   - destruct s; naive_solver.
-  - by rewrite big_sepL_nil right_id.
+  - rewrite /= right_id. by iApply (step_fupd_wand with "Hwp").
 Qed.
 
-Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
-  ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
+  ▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
+  intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
+  induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
 End lifting.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index 4f45acc997caa31396b5a8b3c5ea459580260a9d..3a9a775cebb9c313a8881361ce87bbd3c0b35692 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -70,13 +70,15 @@ Proof.
   by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
-Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
-  PureExec φ e1 e2 →
+Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
   φ →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros ([??] Hφ) "HWP".
-  iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
+  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iApply twp_lift_pure_det_step; [done|naive_solver|].
+  iModIntro. rewrite /= right_id. by iApply "IH".
 Qed.
 
 End lifting.