X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationCategory.v;h=2261f88f61864d3058b7155e7d63d14a8e474ee2;hp=9a7c3fd2720a1a4c1c754b3402f5cdd326ae64a9;hb=2da83e6cfd727f142489859160b7d57bfa80a3be;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 9a7c3fd..2261f88 100644
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -97,6 +97,7 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   apply (ni_respects2 (a >>>> a') (b >>>> b') x).
   apply ni_inv.
   apply comm1.
+  apply (reification_host_lang_pure _ _ _ X0).
   Defined.
 
 Definition reificationOrIdentityComp