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.

Thanks!

I don't think we are very consistent with indenting in particular for big sections, so this should probably be audited before landing.

I manually audited by running rg '(Global Hint|^Section|^End)' theories/ and then looking for any hints between a section start and end - didn't find any, so I think this MR is correct (that is, it should have no outside effect).

This concerns https://github.com/coq/coq/pull/13188 right? If so, please include that in the MR description.

I manually reviewed this MR, and it seems correct.

merged

mentioned in commit 94d45b1c

Thanks!

changed the description

changed the description