The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 27 août 2012 à 12:52, Andreas Abel a écrit :
<snip/>
>> Second: Assuming that this would not cause problems, are there any plans
>> to add this to Coq?

Hello Jason,

  There are plans to add this to Coq real soon, I'm working on the 
implementation.
η for (non-recursive) records will come along with a more efficient 
representation for projections which will not carry parameters anymore (as in 
Agda too).

Cheers,
-- Matthieu