Skip to content

Add explicit Global to hints at top level

Tej Chajed requested to merge tchajed/stdpp:fix-hint-locality into master

Fixes new Coq master warning deprecated-hint-without-locality:

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.

Edited by Tej Chajed

Merge request reports