Trigger the ssr rewrite warning at globalization time.

[ppedrot]

Instead of doing that at runtime, which clutters the output with irrelevant data, we do this at globalization time using an already available mechanism in TACTIC EXTEND.

Note that we lose the quickfix info as there is no way to make a Deprecation.t with a quickfix in the API, should that be fixed first? cc @proux01 and @gares

[SkySkimmer]

This also changes the warning name and message though.

Warning: Tactic Notation rewrite (ssrrewriteargs) (ssrclauses) is deprecated since 9.3.
The 'rewrite' tactic has been renamed 'rw'.
[deprecated-tactic-notation-since-9.3,deprecated-since-9.3,deprecated-tactic-notation,deprecated,default]

instead of

Warning: The 'rewrite' tactic has been renamed 'rw'.
[rewrite-rw,deprecated-since-9.3,deprecated,default]

[ppedrot]

I guess that we could tweak the DEPRECATED clause to accept arbitrary warnings if we want this...

[SkySkimmer]

Best I can come up with is #21877