diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index c50bdef3fe482a16c3527589ba9d440e7f857f22..93e269e73fa8ba8423d143d3914f2e238794b36f 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -118,4 +118,4 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
      : string
 The command has indeed failed with message:
 Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: not a 'wp'.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index bd89e2de2e5c8a470b56f1d3444143ac91ecd695..f00723e452b98894d6ddf2f99f76b921ca709175 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -186,7 +186,7 @@ Section error_tests.
 
   Check "not_cas".
   Lemma not_cas :
-    (WP #() {{ _, True }})%I.
+    (WP #() #() {{ _, True }})%I.
   Proof.
     Fail wp_cas_suc.
   Abort.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index b8dd756beb34a98fc1e16d624cdce32726abc355..6baede50eef36e14ea95ca7a11815514beba296e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -85,8 +85,11 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
-(* The `;[]` makes sure that no side-condition magically spawns. *)
-Ltac wp_pures := repeat (wp_pure _; []).
+(* TODO: do this in one go, without [repeat]. *)
+Ltac wp_pures :=
+  iStartProof;
+  repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
+                             magically spawns. *)
 
 (* The handling of beta-reductions with wp_rec needs special care in
   order to allow it to unlock locked `RecV` values: We first put