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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
index 2af21f922..c44873ee0 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
@@ -49,16 +49,19 @@ Require Export pr3_confluence.
 Require Export pr3_subst1.
 Require Export pr3_gen_context.
 Require Export pc1_defs.
+Require Export pc1_props.
 Require Export pc3_defs.
 Require Export pc3_props.
 Require Export pc3_gen.
 Require Export pc3_subst0.
 Require Export pc3_gen_context.
 Require Export ty0_defs.
+Require Export ty0_gen.
 Require Export ty0_lift.
 Require Export ty0_props.
 Require Export ty0_subst0.
 Require Export ty0_gen_context.
 Require Export csub0_defs.
+Require Export csub0_props.
 Require Export ty0_sred.
 Require Export ty0_sred_props.