One of the definitions of noccur_between is wrong, because the Template one uses an && where the PCUIC one uses ||. I think PCUIC's is the right one, since it's the one where we actually prove things. I guess we didn't catch the issue because we don't use the function from Template anywhere and so we don't prove any of its properties…
I'm working on the 8.19 branch locally (because that's the Coq version I have) so the PR it to that branch, I'll make another one for main :)
One of the definitions of
noccur_betweenis wrong, because the Template one uses an&&where the PCUIC one uses||. I think PCUIC's is the right one, since it's the one where we actually prove things. I guess we didn't catch the issue because we don't use the function from Template anywhere and so we don't prove any of its properties…I'm working on the 8.19 branch locally (because that's the Coq version I have) so the PR it to that branch, I'll make another one for
main:)