X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_subst0.v;h=ffd80110bf4c0dc6591540932d98f980b92a8476;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1da24f50000adf8c4efd8bdd0d412da67f605212;hpb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
index 1da24f500..ffd80110b 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
@@ -4,6 +4,7 @@ Require fsubst0_defs.
 Require pc3_props.
 Require pc3_subst0.
 Require ty0_defs.
+Require ty0_gen.
 Require ty0_lift.
 Require ty0_props.