diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 6e289acc32306ea8615d16b29f33ab53b0898f76..5b681ca30c82b3aeec8fa71ef8ad860ee1855d89 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -27,8 +27,8 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp
   (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
   WP par e {{ Φ }}.
 Proof.
-  iIntros (?) "Hf1 Hf2 HΦ".
-  rewrite /par. wp_value. wp_let. wp_proj.
+  iIntros (<-%of_to_val) "Hf1 Hf2 HΦ".
+  rewrite /par /=. wp_let. wp_proj.
   wp_apply (spawn_spec parN with "Hf1"); try wp_done; try solve_ndisj.
   iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
   iApply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 8f2f4b9615b7061b9deb9740158bf83fa7768890..8e4629a2c7daaba7bd663bed90e892e166fda3f9 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -24,14 +24,6 @@ Ltac wp_done :=
 
 Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; simpl.
 
-Tactic Notation "wp_value" :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
-  | _ => fail "wp_value: not a wp"
-  end.
-
 Lemma of_val_unlock v e : of_val v = e → of_val (locked v) = e.
 Proof. by unlock. Qed.