diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index bd01b72a48afe156209c2d1dd0d4c1dc19ed08de..fa9b31fca7b5346f59c2d60d8c940df6a14dd92e 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
       |env_cbv; reflexivity
-      |wp_finish]
+      |wp_finish; try wp_seq]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 7665f27c63066f69a1c1a3fc54a0afecf47f697e..4d17d5a920579e396c306fb257f0ced2ac34fdaa 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -45,7 +45,7 @@ Section client.
     iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
     iFrame "Hh". iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
+      wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
       iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros {_ _} "_ >"].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 84aa55224e86ba09384dc797cb0362fd38e0d478..61f35795800d3af3edfa4200a8ad71090238b7b5 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -27,7 +27,7 @@ Section LiftingTests.
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
-    wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
+    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
   Qed.
 
   Definition heap_e2  : expr [] :=
@@ -39,7 +39,7 @@ Section LiftingTests.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
-    wp_load. wp_op. wp_store. wp_seq. wp_load. done.
+    wp_load. wp_op. wp_store. wp_load. done.
   Qed.
 
   Definition FindPred : val :=