diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 89c42bdc7c0c11e21bc679fd74d8ed0909750155..250475d299c20cf82064fe50a0edf1db97924875 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -565,7 +565,9 @@ Tactic Notation "iApply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H => first
     [iExact H
     |go H
-    |lazymatch iTypeOf H with Some (_,?Q) => fail "iApply: cannot apply" Q end]).
+    |lazymatch iTypeOf H with
+     | Some (_,?Q) => fail 1 "iApply: cannot apply" Q
+     end]).
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=