we restored the scripts of \lambda\delta version 1

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / LambdaDelta.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
deleted file mode 100644 (file)
index c44873e..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
+++ /dev/null
@@ -1,67 +0,0 @@
-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.
-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.
-Require Export subst0_subst0.
-Require Export subst0_confluence.
-Require Export subst0_tlt.
-Require Export subst1_defs.
-Require Export subst1_gen.
-Require Export subst1_lift.
-Require Export subst1_subst1.
-Require Export subst1_confluence.
-Require Export csubst0_defs.
-Require Export csubst1_defs.
-Require Export fsubst0_defs.
-Require Export pr0_defs.
-Require Export pr0_lift.
-Require Export pr0_gen.
-Require Export pr0_subst0.
-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.
-Require Export pr2_confluence.
-Require Export pr2_subst1.
-Require Export pr2_gen_context.
-Require Export pr3_defs.
-Require Export pr3_props.
-Require Export pr3_gen.
-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.