Add locality for `Hint Rewrite`.

We can do this since we dropped support for Coq 8.13.

For natmap, the apply to internal lemmas and should thus be Local.

For the bit files, it appears the rewrites are used in a tactic that is used externally. Hence they should be Global.

Todo when merging: Remove from https://gitlab.mpi-sws.org/iris/iris/-/wikis/coq-bugs#coq-bugs-recently-fixed-features-recently-introduced-that-we-are-not-yet-taking-advantage-of

added 1 commit

• 7993266d - coq-lint: warn about Hint Rewrite without locality

Compare with previous version

LGTM. I extended coq-lint to also complain about Hint Rewrite with missing locality.

resolved all threads

merged

mentioned in commit 46e72edb

Great. Merging.