Stream: Coq devs & plugin devs

Topic: Warning config as attribute

view this post on Zulip Matthieu Sozeau (Jan 08 2021 at 12:48):

I'm wondering if it would not be a good time to make warnings into attributes. I'd like to write:

#[warnings="-uniform-inheritance"]
Coercion well_subst_usubst : well_subst >-> usubst.

Have we thought about this before?

view this post on Zulip Théo Zimmermann (Jan 08 2021 at 13:40):

Yes, I would like that too.

view this post on Zulip Gaëtan Gilbert (Jan 08 2021 at 15:03):

Currently attributes are processed after parsing and stm, so some warnings would not be affected
other than that it would be easy

view this post on Zulip Théo Zimmermann (Jan 22 2021 at 14:24):

See also the internal but related use case here: https://github.com/coq/coq/pull/13776

Fix #13739 - disable some warnings when calling Function. by Matafou · Pull Request #13776 · coq/coq
Kind: bug fix Fixes / closes #13739 by disabling warnings when calling Function. It also fixes the warning about non truly recursive function. The fix is not entirely satisfactory since Function ...

Last updated: May 28 2023 at 16:30 UTC