Skip to content

Add explicit Local/Global to hints at top level

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

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.

Edited by Tej Chajed

Merge request reports