Small conflict between the proper variables of a let-pattern and the variable in its "as" clause

[herbelin]

Description of the problem

Check fun '(x,y) => eq_refl (x,y).

is displayed as

fun pat : ?T * ?T0 =>
let '(x, y) as x := pat return (x = x) in eq_refl

which is not reinterpretable due to the x of as x is used in the pattern (in addition to being used in the return clause). Being used in the pattern, it clashes with the other x.

Interestingly,

Check fun pat : nat * nat => let '(x, y) := pat in eq_refl (x,y).

does not have the problem. It gives:

fun pat : ?T * ?T0 =>
let '(x, y) as pat0 := pat return (pat0 = pat0) in eq_refl

A fix shall come soon.

Coq Version

A priori all versions since fun 'pat => ... is supported.