Commit 6d37fbe4 authored by Ralf Jung's avatar Ralf Jung

improve IPM deprecation warning

parent feccb48c
......@@ -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) *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment