Stream: Coq devs & plugin devs

Topic: New feature that is currently unusable


view this post on Zulip Yann Leray (Mar 25 2024 at 16:21):

I need to add extensible quality instances for a new development in rewrite rules. It is however easy to isolate, even if currently useless.
Should I make it a PR or wait and include it to that new development ?

view this post on Zulip Gaëtan Gilbert (Mar 25 2024 at 16:46):

please explain more why you need it

view this post on Zulip Yann Leray (Mar 25 2024 at 16:48):

I am going to spawn many new quality variables, and it's dealt with the same way as when there are more universes than given in the univdecl. I don't strictly need it this way, but this would fit and I don't see why it would hurt the rest of the codebase

view this post on Zulip Gaëtan Gilbert (Mar 25 2024 at 17:42):

no need for separate PR I think


Last updated: Oct 13 2024 at 01:02 UTC