The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/19/2017 12:02 PM, Théo Zimmermann wrote:
> Very good point Pierre. And now that you mention this, Matthieu was
> precisely recently talking about the need for anonymous records (which
> would probably be made available by creating a syntax for anonymous
> inductive types, since Coq's record are implemented in terms of inductive
> types).

I'll add my +1 to the anonymous inductives idea as well.  There are 
certainly cases where having that would make things more elegant (such 
as the case where a tactic needs an inductive type to work, but would be 
defeated if that inductive type is used elsewhere).

Oh - but would two syntactically identical anonymous inductives be 
equal?   Hmmm - probaby.  If so, would it be possible to have some way 
to unique-ify an anonymous inductive?

-- Jonathan