]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
some reorganization and some corrections
[helm.git] / helm / coq-contribs / LAMBDA-TYPES / LambdaDelta.v
index ef5b4afbc2374beabfb638c45a92ed46e3be4590..2af21f9227a42cf9ca730c30efed92313928df30 100644 (file)
@@ -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,8 +48,6 @@ 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 pc3_defs.
 Require Export pc3_props.