X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2FMake;h=c895b78c9ad5f9ae18897ba050079c675d836aa7;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=0a3e0514c76aa52d14b4eb3839e1f57b546fb031;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/Make b/helm/coq-contribs/LAMBDA-TYPES/Make index 0a3e0514c..c895b78c9 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/Make +++ b/helm/coq-contribs/LAMBDA-TYPES/Make @@ -12,6 +12,8 @@ lift_defs.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 @@ -23,10 +25,9 @@ subst1_gen.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 @@ -35,6 +36,7 @@ pr0_confluence.v pr0_subst1.v pr1_defs.v pr1_confluence.v +cpr0_defs.v pr2_defs.v pr2_lift.v pr2_gen.v @@ -47,20 +49,21 @@ pr3_gen.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