ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
index 62aa5c3993a1b7d24e20eb59620fe0edf2c412fc..99548beb5220547332feb751a85908151a6c69e5 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
@@ -4,14 +4,17 @@ Require csubst1_defs.
 Require pr0_lift.
 Require pr0_subst1.
 Require cpr0_defs.
+Require pc1_props.
 Require pc3_props.
 Require pc3_gen.
 Require ty0_defs.
+Require ty0_gen.
 Require ty0_lift.
 Require ty0_props.
 Require ty0_subst0.
 Require ty0_gen_context.
 Require csub0_defs.
+Require csub0_props.
 
 (*#* #caption "subject reduction" #clauses *)
 
@@ -178,7 +181,7 @@ Require csub0_defs.
         ]; XEAuto
       | Idtac ].
       Rewrite <- lift_bind; Apply pc3_pc1;
-      Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
+      Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
 (* case 7: ty0_cast *)
       Intros; Inversion H5; Clear H5.
 (* case 7.1: pr0_refl *)
@@ -220,7 +223,7 @@ Require csub0_defs.
 
 (*#* #start file *)
 
-(*#* #caption "general case" *)
+(*#* #caption "general case without the reduction in the context" *)
 (*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
 
       Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->