Adapt to Coq PR #18445, that fixes an issue with multiple signatures of implicit arguments for notations

[herbelin]

PR coq/coq#18445 implements the (originally intended) behaviour for selecting maximal implicit arguments of a notation for an applied constant in the presence of multiple signatures of implicit arguments. Such notation now behaves like ordinary constants or abbreviations for non applied constants, that is, they complete the application with as much implicit arguments as possible.

This impacts the notation "naturality[ x ] := (@naturality _ _ _ _ x)" which comes with 3 different signatures of implicit arguments. It is now resolved by default with 3 trailing implicit arguments, making tactics such as a srewrite (naturality[unit]) later failing with unresolved arguments (e.g. in Adjunction/Hom.v).

It happens that the naturality constant is mostly used in practice with only one signature of implicit arguments. So, the proposed adaptation is to restrict naturality to only this signature.

This is of course not the only way to adapt to coq/coq#18445. Another approach would be e.g. to use e-tactics so that srewrite accepts to leave unresolved the added implicit arguments.

In any cases, the PR is backwards-compatible and can be merged as soon as now.

[proux01]

@jwiegley could this be merged please? We need it in order to merge https://github.com/coq/coq/pull/18445 in Coq.

[jwiegley]

@proux01 Thank you for the ping, I somehow missed this notification e-mail last week.

[proux01]

No worries, thanks!