Just out of curiosity, is there any major blocker to removing the last uses of the V82 compat layer, or is it just a matter of spending a bit of time?
funind is going to be a lot of efforts
but just because there are lots of occurrences? or some missing functionality?
With funind I got far enough as to have only one real blocker
some very weird manipulation that I couldn't manage, but that should be doable
so you have a branch that removes most uses of the V82 compat layer?
I indeed still have some commits here and there
but they are very routine
I got blocked on that weird destruct stuff
also some evar_maps are passed by ref and they are quite hard to understand
recently I cleaned up a few
so indeed it would make sense to do a pass
but likely we want to leave funind for the last
what about ssreflect tho?
with funind my understanding is that easily we will be down to 2 / 3 problematic places
yeah ssr is also why I was asking if there were "real" blockers
I guess we are still going to hit the lack of evar garbage collection issue
@Pierre-Marie Pédrot I have a related question: what does the comment at https://github.com/coq/coq/blob/c077db40a204132eda8a5d5979022f4961503cab/engine/proofview.ml#L754 mean?
i.e. why can future goals come only from the compat layer at that code point?
Last updated: Oct 16 2021 at 03:02 UTC