update baked in CoqPass.hs

[coq-hetmet.git] / src / GeneralizedArrowCategory.v

diff --git a/src/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v
index 3a6a74a..745484b 100644 (file)
--- a/src/GeneralizedArrowCategory.v
+++ b/src/GeneralizedArrowCategory.v
@@ -62,6 +62,8 @@ Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1
 Instance compose_generalizedArrows (s0 s1 s2:SMMEs) 
   (g01:GeneralizedArrow s0 s1)(g12:GeneralizedArrow s1 s2) : GeneralizedArrow s0 s2 :=
     { ga_functor_monoidal := g01 >>⊗>> smme_mon s1 >>⊗>> g12 }.
+  apply ga_host_lang_pure.
+  Defined.
 
 Definition generalizedArrowOrIdentityComp
   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.