The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Cedric,

Thank you for the information. My conclusion is that I will be
replacing most, if not all, of the Records that I have in my code by
Inductives as I simply cannot stomach the new Record notation. The
nice thing about the Records used to be that the field names can be
used to get a field from a Record. So, I will turn the field names
that I need in separate Definitions with match-constructions. This
would seem to solve the problem for me. Fortunately I was not using
that many different Record types anyway.

Cedric and/or others might want to consider providing a "Set Printing"
option for switching this new notation display off. If I feel like it
I might even create a feature request in the bugzilla.

All the best,
Chris