X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2FMakefile;h=1648c32aaf05e10e53e5760fd925c4a6941e085d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=b3936376b3b42e8d1a66de06d22ef7c73dff5808;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/Makefile b/helm/coq-contribs/LAMBDA-TYPES/Makefile
index b3936376b..1648c32aa 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/Makefile
+++ b/helm/coq-contribs/LAMBDA-TYPES/Makefile
@@ -75,6 +75,8 @@ VFILES=base_tactics.v\
   lift_gen.v\
   lift_props.v\
   lift_tlt.v\
+  drop_defs.v\
+  drop_props.v\
   subst0_defs.v\
   subst0_gen.v\
   subst0_lift.v\
@@ -86,10 +88,9 @@ VFILES=base_tactics.v\
   subst1_lift.v\
   subst1_subst1.v\
   subst1_confluence.v\
-  drop_defs.v\
-  drop_props.v\
   csubst0_defs.v\
   csubst1_defs.v\
+  fsubst0_defs.v\
   pr0_defs.v\
   pr0_lift.v\
   pr0_gen.v\
@@ -98,6 +99,7 @@ VFILES=base_tactics.v\
   pr0_subst1.v\
   pr1_defs.v\
   pr1_confluence.v\
+  cpr0_defs.v\
   pr2_defs.v\
   pr2_lift.v\
   pr2_gen.v\
@@ -110,20 +112,21 @@ VFILES=base_tactics.v\
   pr3_confluence.v\
   pr3_subst1.v\
   pr3_gen_context.v\
-  cpr0_defs.v\
-  cpr0_props.v\
   pc1_defs.v\
+  pc1_props.v\
   pc3_defs.v\
   pc3_props.v\
   pc3_gen.v\
   pc3_subst0.v\
   pc3_gen_context.v\
   ty0_defs.v\
+  ty0_gen.v\
   ty0_lift.v\
   ty0_props.v\
   ty0_subst0.v\
   ty0_gen_context.v\
   csub0_defs.v\
+  csub0_props.v\
   ty0_sred.v\
   ty0_sred_props.v\
   LambdaDelta.v
@@ -146,6 +149,8 @@ all: base_tactics.vo\
   lift_gen.vo\
   lift_props.vo\
   lift_tlt.vo\
+  drop_defs.vo\
+  drop_props.vo\
   subst0_defs.vo\
   subst0_gen.vo\
   subst0_lift.vo\
@@ -157,10 +162,9 @@ all: base_tactics.vo\
   subst1_lift.vo\
   subst1_subst1.vo\
   subst1_confluence.vo\
-  drop_defs.vo\
-  drop_props.vo\
   csubst0_defs.vo\
   csubst1_defs.vo\
+  fsubst0_defs.vo\
   pr0_defs.vo\
   pr0_lift.vo\
   pr0_gen.vo\
@@ -169,6 +173,7 @@ all: base_tactics.vo\
   pr0_subst1.vo\
   pr1_defs.vo\
   pr1_confluence.vo\
+  cpr0_defs.vo\
   pr2_defs.vo\
   pr2_lift.vo\
   pr2_gen.vo\
@@ -181,20 +186,21 @@ all: base_tactics.vo\
   pr3_confluence.vo\
   pr3_subst1.vo\
   pr3_gen_context.vo\
-  cpr0_defs.vo\
-  cpr0_props.vo\
   pc1_defs.vo\
+  pc1_props.vo\
   pc3_defs.vo\
   pc3_props.vo\
   pc3_gen.vo\
   pc3_subst0.vo\
   pc3_gen_context.vo\
   ty0_defs.vo\
+  ty0_gen.vo\
   ty0_lift.vo\
   ty0_props.vo\
   ty0_subst0.vo\
   ty0_gen_context.vo\
   csub0_defs.vo\
+  csub0_props.vo\
   ty0_sred.vo\
   ty0_sred_props.vo\
   LambdaDelta.vo
@@ -227,6 +233,8 @@ xml:: .xml_time_stamp
   lift_gen.vo\
   lift_props.vo\
   lift_tlt.vo\
+  drop_defs.vo\
+  drop_props.vo\
   subst0_defs.vo\
   subst0_gen.vo\
   subst0_lift.vo\
@@ -238,10 +246,9 @@ xml:: .xml_time_stamp
   subst1_lift.vo\
   subst1_subst1.vo\
   subst1_confluence.vo\
-  drop_defs.vo\
-  drop_props.vo\
   csubst0_defs.vo\
   csubst1_defs.vo\
+  fsubst0_defs.vo\
   pr0_defs.vo\
   pr0_lift.vo\
   pr0_gen.vo\
@@ -250,6 +257,7 @@ xml:: .xml_time_stamp
   pr0_subst1.vo\
   pr1_defs.vo\
   pr1_confluence.vo\
+  cpr0_defs.vo\
   pr2_defs.vo\
   pr2_lift.vo\
   pr2_gen.vo\
@@ -262,20 +270,21 @@ xml:: .xml_time_stamp
   pr3_confluence.vo\
   pr3_subst1.vo\
   pr3_gen_context.vo\
-  cpr0_defs.vo\
-  cpr0_props.vo\
   pc1_defs.vo\
+  pc1_props.vo\
   pc3_defs.vo\
   pc3_props.vo\
   pc3_gen.vo\
   pc3_subst0.vo\
   pc3_gen_context.vo\
   ty0_defs.vo\
+  ty0_gen.vo\
   ty0_lift.vo\
   ty0_props.vo\
   ty0_subst0.vo\
   ty0_gen_context.vo\
   csub0_defs.vo\
+  csub0_props.vo\
   ty0_sred.vo\
   ty0_sred_props.vo\
   LambdaDelta.vo