The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/31/2016 11:18 PM, Jason Gross wrote:
> Actually, I think it's possible to do better; you should only need
> AtoB_BtoA specialized to the point you care about.  This should be a
> relatively simple transformation to make, and, I think, should be powerful
> enough to let you handle recursive types

I think you are right that AtoB_BtoA only needs to be at a point. But, 
if AtoB is always a ctor and BtoA is always a proj, then I'm not sure 
that this specialization helps much, if at all.

-- Jonathan