diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a793ec715a52a385be8c8dc8d6faf7566faa516e..2a891fa17d615b7eeb75c34a68cc41b427f4531b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -219,12 +219,16 @@ Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
-  iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext; simpl)
-  | _ => fail "wp_apply: not a 'wp'"
-  end.
+  iPoseProofCore lem as false true (fun H =>
+    lazymatch goal with
+    | |- _ ⊢ wp ?E ?e ?Q =>
+      reshape_expr e ltac:(fun K e' =>
+        wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "wp_apply: cannot apply" P
+      end
+    | _ => fail "wp_apply: not a 'wp'"
+    end).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ae579767943a92a7603e99ecc2fd8e38c123a73f..3ae23afbedf8397af9d13387cb2b8dfc0fa7dd08 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -564,19 +564,21 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
   end.
 
 (** * Apply *)
-Tactic Notation "iApply" open_constr(lem) :=
+Tactic Notation "iApplyHyp" constr(H) :=
   let rec go H := first
     [eapply tac_apply with _ H _ _ _;
       [env_reflexivity
       |apply _
       |lazy beta (* reduce betas created by instantiation *)]
     |iSpecializePat H "[]"; last go H] in
-  iPoseProofCore lem as false true (fun H => first
-    [iExact H
-    |go H
-    |lazymatch iTypeOf H with
-     | Some (_,?Q) => fail 1 "iApply: cannot apply" Q
-     end]).
+  iExact H ||
+  go H ||
+  lazymatch iTypeOf H with
+  | Some (_,?Q) => fail "iApply: cannot apply" Q
+  end.
+
+Tactic Notation "iApply" open_constr(lem) :=
+  iPoseProofCore lem as false true (fun H => iApplyHyp H).
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=