Merge pull request #137 from herbelin/master+adapt-coq-pr18445-fix-ap…

…plied-notations-multiple-implicit
jwiegley · Jan 9, 2024 · e50af05 · e50af05
2 parents 41ab38d + 5089fc0
commit e50af05
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/Theory/Natural/Transformation.v b/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).