Skip to content

Add locality for `Hint Rewrite`.

Robbert Krebbers requested to merge robbert/hint_rewrite_locality into master

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.

Merge request reports