diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 95ae906c193c924994399d273968507f390feb54..a31e6f7e22ef60cfd0ad7bc7fb6398bfbe7e277b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -408,7 +408,7 @@ End heap.
 [wp_bind K; tac H] for every possible evaluation context.  [tac] can do
 [iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
 happens *after* [tac H] got executed. *)
-Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
+Tactic Notation "wp_apply_core" open_constr(lem) tactic3(tac) :=
   wp_pures;
   iPoseProofCore lem as false (fun H =>
     lazymatch goal with
@@ -435,10 +435,10 @@ the context, which is intended to be the non-laterable assertions that iAuIntro
 would choke on.  You get them all back in the continuation of the atomic
 operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  (wp_apply_core lem (fun H => iApplyHyp H));
+  wp_apply_core lem (fun H => iApplyHyp H);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
-  (wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]));
+  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]);
   last iAuIntro.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=