ocaml 3.09 transition

[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
index 2af21f9227a42cf9ca730c30efed92313928df30..c44873ee0fa6bd69d375d37169a145e3042ea4bc 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v
@@ -49,16 +49,19 @@ 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.