diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index fa9b31fca7b5346f59c2d60d8c940df6a14dd92e..bd01b72a48afe156209c2d1dd0d4c1dc19ed08de 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; try wp_seq]
+      |wp_finish]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 4f42702a81d0f10a813216d5f0abd87b0b289aef..aa27dd003b4a7e6363b37fe374547fecf3e6908a 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -22,8 +22,14 @@ Ltac wp_value_head :=
       match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
   end.
 
+Ltac wp_seq_head :=
+  lazymatch goal with
+  | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; strip_later
+  end.
+
 Ltac wp_finish := intros_revert ltac:(
-  rewrite /= ?to_of_val; try strip_later; try wp_value_head).
+  rewrite /= ?to_of_val; try strip_later; try wp_value_head);
+  repeat wp_seq_head.
 
 Tactic Notation "wp_value" :=
   lazymatch goal with