diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a9d2d5f3aa5b7c2a2eaba39ea2bc0562d48ca318..5801ae991352c2165e474ce612f38f3b3cd22cae 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,15 +5,6 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
-
 Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
@@ -26,6 +17,8 @@ Proof.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
+Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
+
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
@@ -54,6 +47,12 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  end.
+
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with