Stream: Coq devs & plugin devs

Topic: Error on hint absence


view this post on Zulip Karl Palmskog (Sep 20 2022 at 15:19):

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

view this post on Zulip Karl Palmskog (Sep 20 2022 at 15:21):

prompted by: https://github.com/coq/opam-coq-archive/pull/2316


Last updated: Dec 07 2023 at 14:02 UTC