Removing a source of clash with multiple recursive patterns in notations.

The same variable name was used to collect the binders and the
successive steps of matching one binder, resulting in unexpected
attempts for merging in the presence of multiple occurrence of the
same recursive pattern.

An amusing side-effect: when eta-expanding for a notation with
recursive binders, it is the second variable of the "x .. y" which is
used to invent a name rather than the first one.

0 files changed, 0 insertions, 0 deletions