The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

We started to play around with primitive projections a little in our
development, and if they work (which unfortunately still is a rather big
if), we could achieve some fairly significant performance improvements:
Coq 8.6 got >7% faster (that's total compilation time!) by switching the
record we use for sealing some of our core definitions to primitive
projections. That's pretty impressive!

One thing we couldn't figure out though is when we get eta conversion
for primitive projections.  The aforementioned record used for sealing
does not have eta (according to About), while other records do.  Are the
rules for when a primitive record gets eta written down anywhere?  All I
could find in the documentation is the two paragraphs in
<https://coq.inria.fr/distrib/8.6beta1/refman/Reference-Manual004.html>,
which don't even mention that primitive projections have anything to do
with eta conversion.

Kind regards,
Ralf