Add explicit Global to hints at top level
- Nov 20, 2020
-
-
Tej Chajed authored
Fixes new Coq master warning deprecated-hint-without-locality.
Verified8e8f3a41
-
Fixes new Coq master warning deprecated-hint-without-locality: https://github.com/coq/coq/pull/13384.
I created this largely automatically based on the assumption that hints in sections would be indented. If some aren't, this MR will change them to global when they should be left alone (implicitly as local). I haven't carefully audited that this didn't happen.
Fixes new Coq master warning deprecated-hint-without-locality.