Stream: Coq devs & plugin devs

Topic: UnivSubst.nf_evars_and_universes_opt_subst deprecation


view this post on Zulip Matthieu Sozeau (Sep 23 2024 at 13:56):

I don't understand why this function is deprecated in favor of a more general function which doesn't expand evars, the only way I can adapt equations is to copy the code from Coq's source code. @Gaëtan Gilbert

view this post on Zulip Gaëtan Gilbert (Sep 23 2024 at 15:01):

this one is from @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2024 at 15:04):

IIRC it's very inefficient compared to the other function

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2024 at 15:09):

why do you need to expand evars in Equations btw ? there is only one call to nf_evars_and_universes_opt_subst and it's not clear from the function definition that it requires expanded evars

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2024 at 15:09):

the code looks wrong, you should first collect the qualities from the term, then collapse them in the evar map and finally nf-evar the term

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2024 at 15:10):

not make a single-pass mixing one and a half of that

view this post on Zulip Matthieu Sozeau (Sep 23 2024 at 15:11):

I don't believe it's me who wrote this code :)

view this post on Zulip Matthieu Sozeau (Sep 23 2024 at 15:11):

There is no expansion in that function actually, my bad

view this post on Zulip Matthieu Sozeau (Sep 23 2024 at 15:12):

So I can switch to the map_ function fine


Last updated: Oct 13 2024 at 01:02 UTC