I'm getting a bunch of deprecated-hint-without-locality warnings on fiat-crypto. It's easy to fix many of them just by adding
Global Hint Rewrite is an error in Coq 8.9 (which we support as it's the version on the latest Debian stable; when Bullseye becomes stable, I expect we'll be open to dropping support for 8.9 and 8.10 and bump the minimum version to 8.11, which is what's packaged on the latest Ubuntu LTS, focal). Is there a good way to be future compatible here while still supporting Coq 8.9?
There is no simple solution to this, no. But note that it may take a while before the default locality is actually changed, so it's fine to delay these new annotations a bit and silence the warning in the meantime.
One of the hint commands still rejects Global in 8.13 and IIRC that's Hint Rewrite.
Last updated: Oct 01 2023 at 18:01 UTC