Add explicit Global to hints at top level

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.