It seems that, to unfold primitive projection
foo (I don't mean the wrapper), I need
progress cbv beta delta [foo] not just
progress cbv delta [foo]. Is that expected? I do realize this matches the behavior for usual projections, since those are wrappers over lambdas.
This is https://github.com/coq/coq/commit/978ae7d9323558099efb0c4e4e39549221378d5d
IMHO this is an anti-feature but it's too late to fix this kind of code without wreaking havoc...
Makes sense, thanks!
and the new behavior should be part of a larger redesign such as https://github.com/coq/ceps/pull/57.
Last updated: Sep 26 2023 at 13:01 UTC