Fixes #13432: regression with notations involving coercions caused by #11172.

In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".

Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.

Incidentally, we create a dedicated output file for notations and
coercions.

0 files changed, 0 insertions, 0 deletions