diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a70bacbf2ca8460249ec4ba8c4dad8bd07612cf5..cd4b760209e71798be20077b45ffa79a17f3590e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -441,7 +441,7 @@ Tactic Notation "iApply" open_constr(lem) :=
       |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|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
+    first [iExact H|go H|iTypeOf H (fun _ Q => fail "iApply: cannot apply" Q)]).
 
 (** * Revert *)
 Local Tactic Notation "iForallRevert" ident(x) :=