Fixing unexpected length of context in a typing function, detected by

cleaning done in e8c47b652a0.

It had no serious consequences except having whd-reduction blocked on
a let-in when typing a return clause with let-ins in the arity (a
priori resulting in return types of the form e.g. "(let x:=t in fun y
=> T) u" instead of T[x:=t;y:=u], if I'm not mistaking).

This fixes 3210.v in test-suite.

0 files changed, 0 insertions, 0 deletions