From 18d94149267db9cf2e8e93977c5506278309173d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 27 Mar 2011 17:23:40 -0700 Subject: [PATCH] make mf_compose_coherence transparent --- src/MonoidalCategories_ch7_8.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v index e07d035..b7d80a0 100644 --- a/src/MonoidalCategories_ch7_8.v +++ b/src/MonoidalCategories_ch7_8.v @@ -430,7 +430,7 @@ Section MonoidalFunctorsCompose. apply ni_inv. apply mc1. apply ni_id. - Qed. + Defined. Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) := { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1)) -- 1.7.10.4