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
this one is from @Pierre-Marie Pédrot
IIRC it's very inefficient compared to the other function
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
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
not make a single-pass mixing one and a half of that
I don't believe it's me who wrote this code :)
There is no expansion in that function actually, my bad
So I can switch to the map_ function fine
Last updated: Oct 13 2024 at 01:02 UTC