The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 17/09/2017 03:57, Jasper Hugunin wrote:

> I don't think your primitive record example quite works; I would hope
> that when checking
> Rec (t.(p₀), ..., t.(pₙ)) ≡ u,
> u gets expanded so we have
> Rec (t.(p₀), ..., t.(pₙ)) ≡ Rec (u.(p₀), ..., u.(pₙ)).

The actual rule is even more generic: when it fails to ensure

  Rec (t₀, ..., tₙ) ≡ u,

the kernel turns it into

  Rec (t₀, ..., tₙ) ≡ Rec (u.(p₀), ..., u.(pₙ)).

There are no projections on the left-hand side, a priori.

Best regards,

Guillaume