Add explicit Local/Global to hints at top level

Fixes new Coq master warning deprecated-hint-without-locality (https://github.com/coq/coq/pull/13384). While we're at it, also add Local to the other hints.