]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/Make
contribution about \lambda-\delta
[helm.git] / helm / coq-contribs / LAMBDA-TYPES / Make
diff --git a/helm/coq-contribs/LAMBDA-TYPES/Make b/helm/coq-contribs/LAMBDA-TYPES/Make
new file mode 100644 (file)
index 0000000..0a3e051
--- /dev/null
@@ -0,0 +1,66 @@
+# List of vernac files to compile
+base_tactics.v
+base_hints.v
+base_types.v
+base_blt.v
+base_rewrite.v
+Base.v
+terms_defs.v
+tlt_defs.v
+contexts_defs.v
+lift_defs.v
+lift_gen.v
+lift_props.v
+lift_tlt.v
+subst0_defs.v
+subst0_gen.v
+subst0_lift.v
+subst0_subst0.v
+subst0_confluence.v
+subst0_tlt.v
+subst1_defs.v
+subst1_gen.v
+subst1_lift.v
+subst1_subst1.v
+subst1_confluence.v
+drop_defs.v
+drop_props.v
+csubst0_defs.v
+csubst1_defs.v
+pr0_defs.v
+pr0_lift.v
+pr0_gen.v
+pr0_subst0.v
+pr0_confluence.v
+pr0_subst1.v
+pr1_defs.v
+pr1_confluence.v
+pr2_defs.v
+pr2_lift.v
+pr2_gen.v
+pr2_confluence.v
+pr2_subst1.v
+pr2_gen_context.v
+pr3_defs.v
+pr3_props.v
+pr3_gen.v
+pr3_confluence.v
+pr3_subst1.v
+pr3_gen_context.v
+cpr0_defs.v
+cpr0_props.v
+pc1_defs.v
+pc3_defs.v
+pc3_props.v
+pc3_gen.v
+pc3_subst0.v
+pc3_gen_context.v
+ty0_defs.v
+ty0_lift.v
+ty0_props.v
+ty0_subst0.v
+ty0_gen_context.v
+csub0_defs.v
+ty0_sred.v
+ty0_sred_props.v
+LambdaDelta.v