The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Le 06/11/2013 14:34, Cyril Cohen a écrit :
> Christian, when you declare canonical a record where not all the fields are
> named, there is no "proj" to be registered in the canonical structure table 
> (as
> described by Beta) and it's ok because we don't want all projections to be
> registered.

Oh, and I should have made explicit that given a value to declare as 
canonical,
each pair (proj, const) is treated independently from the other projections of
the record. Thus, some pairs may be registered while other won't (if the proj
is unnamed, if const isn't registrable or if the same pair (proj, const) has
already been registered).

-- 
Cyril
sorry for posting in this messy way