Add explicit Local/Global to hints at top level (!594) · Merge requests · Iris / Iris

Merged Tej Chajed requested to merge tchajed/iris-coq:fix-hint-locality into master Nov 27, 2020

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 Dec 03, 2020 by Tej Chajed

Add explicit Local/Global to hints at top level

Merge request reports