From 6d37fbe4d449c809bf709584bdff2c3e72cf18b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Dec 2017 19:52:18 +0100
Subject: [PATCH] improve IPM deprecation warning
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 36b2006c6..288816522 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) *)
--
GitLab