note since when the things recommended in a deprecation note are supported

[RalfJung]

See #15802 (comment)
Cc @Zimmi48

[ppedrot]

Why not the same for all hint-like locality-free deprecated commands?

[RalfJung]

Those are the ones I knew about and cared about enough to do the research required (find out which Coq version the locality was first supported in).

How many more of these warnings are there?

[ppedrot]

$ git grep "The default value for" -- '*.ml'
tactics/autorewrite.ml:    (fun () -> strbrk "The default value for rewriting hint locality is currently \
tactics/hints.ml:    (fun () -> strbrk "The default value for hint locality is currently \
vernac/classes.ml:  "The default value for Typeclasses Opaque and Typeclasses \
vernac/classes.ml:    (fun () -> strbrk "The default value for instance locality is currently \

[RalfJung]

For the other Hint and for Instance, this has been supported since forever, right?

[ppedrot]

At some point we didn't have attributes but only command modifiers, so it depends on how you phrase the claim.

[RalfJung]

Looks like #[local] Lemma foo : bar is supported since Coq 8.9. That counts as "forever".

So I don't know other warnings that would currently benefit from this kind of information.

[ppedrot]

OK, fine with me then.

[ppedrot]

@coqbot merge now