Paolo Giarrusso (Aug 30 2021 at 12:33): Paolo Giarrusso (Aug 30 2021 at 12:33):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.
Pierre-Marie Pédrot (Aug 30 2021 at 12:36):This is https://github.com/coq/coq/commit/978ae7d9323558099efb0c4e4e39549221378d5d
Pierre-Marie Pédrot (Aug 30 2021 at 12:37):IMHO this is an anti-feature but it's too late to fix this kind of code without wreaking havoc...
Paolo Giarrusso (Aug 30 2021 at 13:40):Makes sense, thanks!
Paolo Giarrusso (Aug 30 2021 at 14:29):and the new behavior should be part of a larger redesign such as https://github.com/coq/ceps/pull/57.
Last updated: Oct 13 2024 at 01:02 UTC