diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a31e6f7e22ef60cfd0ad7bc7fb6398bfbe7e277b..d1632a886c41ec2fb8b5787ec375480c84a1eda0 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -16,7 +16,7 @@ Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
 
-Tactic Notation "wp_expr_eval" tactic(t) :=
+Tactic Notation "wp_expr_eval" tactic3(t) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>