Just a general comment, I think these kinds of error messages are terrible:
Error: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. [...]
I understand that the warning was changed into an error, but can't we have error messages sounding like actual errors? Just something like:
Error: Missing locality declaration
prompted by: https://github.com/coq/opam-coq-archive/pull/2316
Last updated: Dec 07 2023 at 14:02 UTC