From 3fe04f47336c98410cfba4ec9827163e9cd770a8 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 30 Jan 2024 17:10:09 -0800 Subject: [PATCH] Be more explicit in Functor/Traversable/Product.v --- Functor/Traversable/Product.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Functor/Traversable/Product.v b/Functor/Traversable/Product.v index 03091252..40f0ddb0 100644 --- a/Functor/Traversable/Product.v +++ b/Functor/Traversable/Product.v @@ -40,8 +40,8 @@ Proof. rewrite comp_assoc. rewrites. rewrite <- !comp_assoc. - pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *. - pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *. + pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *. + pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *. rewrite !comp_assoc. comp_left. rewrite bimap_fmap. @@ -55,8 +55,8 @@ Proof. rewrite comp_assoc. rewrites. rewrite <- !comp_assoc. - pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *. - pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *. + pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *. + pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *. rewrite !comp_assoc. comp_left. rewrite bimap_fmap.