X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;fp=src%2FMonoidalCategories_ch7_8.v;h=b7d80a05fed634aa811c169103fefd67fa884752;hp=e07d03501bcefd716498fabea645a344a26f116e;hb=18d94149267db9cf2e8e93977c5506278309173d;hpb=1ab46a0e579ec1964ae0ab3cadb64f6a77db8d30

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))