Adapt to Coq PR #18845 fixing an issue with maximal implicit argument…

…s for notations.

The new (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 notations now behave
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 is now resolved with 3 trailing implicit arguments, making
tactics such as a "srewrite (naturality[foo])" failing with unresolved
arguments.

It happens that the "naturality" constant mostly uses one signature of
implicit arguments. So, the adaptation is to restrict "naturality" to
only this signature.

Theory/Natural/Transformation.v

@@ -46,10 +46,8 @@ Qed.
 End Transform.
 
 Arguments transform {_ _ _ _} _ _.
-Arguments naturality
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
-Arguments naturality_sym
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
+Arguments naturality {_ _ _ _} _ _ _ _.
+Arguments naturality_sym {_ _ _ _} _ _ _ _.
 
 Declare Scope transform_scope.
 Declare Scope transform_type_scope.
@@ -214,8 +212,8 @@ Program Definition whisker_right {C D : Category} {F G : C ⟶ D} `(N : F ⟹ G)
         {E : Category} (X : E ⟶ C) : F ◯ X ⟹ G ◯ X := {|
   transform := λ x, N (X x);
 
-  naturality     := λ _ _ _, naturality;
-  naturality_sym := λ _ _ _, naturality_sym
+  naturality     := λ _ _ _, naturality _ _ _ _;
+  naturality_sym := λ _ _ _, naturality_sym _ _ _ _
 |}.
 
 Notation "N ⊲ F" := (whisker_right N F) (at level 10).