Fixing #4932 (anomaly when using binders as terms in recursive notations).

This application was actually not anticipated. It is nice and was not
too difficult to support.

Design for pattern binders maybe to clarify. When seing pat(x1,..,xn)
as a term, I just reused pat(x1,..,xn), but maybe it is worth using
the variable aliasing the pattern, for more a concise notation. But at
the same time, this means exposing the internal name of the alias
which is not so elegant.

0 files changed, 0 insertions, 0 deletions