diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 109958a5c95ecef365280e11671ff4835e5bc21f..3052cf2efa1e23d0b5259df7951d282cbec34451 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -47,7 +47,7 @@ Section tests.
       Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
     {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}.
   Proof.
-    iIntros (Φ) "[Hp1 Hp2] HΦ".
+    iIntros (Φ) "[Hp1 Hp2] HΦ". wp_pures.
     wp_apply (wp_resolve with "Hp1"); first done.
     wp_apply (wp_resolve with "Hp2"); first done.
     wp_op.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 39f21d758b1be6aa9a7873f715b9b89832dcb966..38076802bd9a1a17afd99f0b4521b177f3a92e2e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -482,19 +482,28 @@ End heap.
 [wp_bind K; tac H] for every possible evaluation context.  [tac] can do
 [iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
 happens *after* [tac H] got executed. *)
+Ltac wp_pures_reshape_expr tac :=
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [ reshape_expr e ltac:(fun K e' => wp_bind_core K; tac K e')
+      | wp_pure _; [wp_pures_reshape_expr tac] ]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [ reshape_expr e ltac:(fun K e' => twp_bind_core K; tac K e')
+      | wp_pure _; [wp_pures_reshape_expr tac] ]
+  end.
+
 Tactic Notation "wp_apply_core" open_constr(lem) tactic3(tac) :=
-  wp_pures;
   iPoseProofCore lem as false (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-      reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; tac H) ||
+      wp_pures_reshape_expr ltac:(fun K e' => tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
-      reshape_expr e ltac:(fun K e' =>
-        twp_bind_core K; tac H) ||
+      wp_pures_reshape_expr ltac:(fun K e' => tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end