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?
Yes, I would like that too.
Currently attributes are processed after parsing and stm, so some warnings would not be affected
other than that it would be easy
See also the internal but related use case here: https://github.com/coq/coq/pull/13776
Last updated: Dec 05 2023 at 05:01 UTC