From 4482ec20d83ddb2b09d94d625c978992a32e6aff Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 30 Jan 2024 16:46:52 -0800 Subject: [PATCH] Make more uses explicit --- Theory/Kan/Extension.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Theory/Kan/Extension.v b/Theory/Kan/Extension.v index c2a8f3d6..d7a4027e 100644 --- a/Theory/Kan/Extension.v +++ b/Theory/Kan/Extension.v @@ -187,11 +187,11 @@ Proof. * simpl. rewrite <- to_adj_nat_l. rewrite <- to_adj_nat_r. - now srewrite (naturality[X0]). + now srewrite (@naturality _ _ _ _ X0 _ _ f). * simpl. rewrite <- to_adj_nat_l. rewrite <- to_adj_nat_r. - now srewrite (naturality[X0]). + now srewrite (@naturality _ _ _ _ X0 _ _ f). + simpl. proper. apply to_adj_respects. @@ -204,11 +204,11 @@ Proof. * simpl. rewrite <- from_adj_nat_l. rewrite <- from_adj_nat_r. - now srewrite (naturality[X0]). + now srewrite (@naturality _ _ _ _ X0 _ _ f). * simpl. rewrite <- from_adj_nat_l. rewrite <- from_adj_nat_r. - now srewrite (naturality[X0]). + now srewrite (@naturality _ _ _ _ X0 _ _ f). + simpl. proper. apply from_adj_respects.