diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 715f44171968ff1e35aea7734bca24b606dc1c7c..b1d0ffd9746445c09fb2402fb69aba2045f7dede 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -275,7 +275,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
        eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *)
          [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
          |let P := match goal with |- IntoForall ?P _ => P end in
-          apply _ || fail 1 "iSpecialize:" P "not a forall or not a forall of the right type"
+          apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x
          |env_cbv; reflexivity|go xs]
     end in
   go xs.