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=ef5b4afbc2374beabfb638c45a92ed46e3be4590;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
index ef5b4afbc..c44873ee0 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
@@ -1,3 +1,9 @@
+Require Export base_tactics.
+Require Export base_hints.
+Require Export base_types.
+Require Export base_blt.
+Require Export base_rewrite.
+Require Export Base.
 Require Export terms_defs.
 Require Export tlt_defs.
 Require Export contexts_defs.
@@ -5,6 +11,8 @@ Require Export lift_defs.
 Require Export lift_gen.
 Require Export lift_props.
 Require Export lift_tlt.
+Require Export drop_defs.
+Require Export drop_props.
 Require Export subst0_defs.
 Require Export subst0_gen.
 Require Export subst0_lift.
@@ -16,10 +24,9 @@ Require Export subst1_gen.
 Require Export subst1_lift.
 Require Export subst1_subst1.
 Require Export subst1_confluence.
-Require Export drop_defs.
-Require Export drop_props.
 Require Export csubst0_defs.
 Require Export csubst1_defs.
+Require Export fsubst0_defs.
 Require Export pr0_defs.
 Require Export pr0_lift.
 Require Export pr0_gen.
@@ -28,6 +35,7 @@ Require Export pr0_confluence.
 Require Export pr0_subst1.
 Require Export pr1_defs.
 Require Export pr1_confluence.
+Require Export cpr0_defs.
 Require Export pr2_defs.
 Require Export pr2_lift.
 Require Export pr2_gen.
@@ -40,19 +48,20 @@ Require Export pr3_gen.
 Require Export pr3_confluence.
 Require Export pr3_subst1.
 Require Export pr3_gen_context.
-Require Export cpr0_defs.
-Require Export cpr0_props.
 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.