Jason Gross (Mar 03 2021 at 13:34): Jason Gross (Mar 03 2021 at 13:34):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. However, 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?
Théo Zimmermann (Mar 03 2021 at 13:54):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.
Paolo Giarrusso (Mar 03 2021 at 14:17):One of the hint commands still rejects Global in 8.13 and IIRC that's Hint Rewrite.
Théo Zimmermann (Mar 03 2021 at 14:41):Right.
Last updated: Oct 13 2024 at 01:02 UTC