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.
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.