Merged requested to merge robbert/hint_rewrite_locality into master
We can do this since we dropped support for Coq 8.13.
natmap, the apply to internal lemmas and should thus be
For the bit files, it appears the rewrites are used in a tactic that is used externally. Hence they should be