diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 36b2006c69cf4e84e586c22de6f0ae4b7bcf3f90..288816522756d079943c781dbcf1193ba221ea90 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -411,7 +411,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
     lazymatch pats with
     | [] => idtac
     | SForall :: ?pats =>
-       idtac "the * specialization pattern is deprecated because it is applied implicitly";
+       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
        go H1 pats
     | SIdent ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)