ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
index 0b634e59c8c314a4d90a7ad5817b64f3b0b2ec56..bfe189586eccd8980d69d0d5c31fbfad0514aa0a 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v
@@ -44,16 +44,11 @@ Require pr0_lift.
                XElim H_x; Intro; Intros H_x; Intro;
                Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
 
-(*#* #start file *)
-
 (*#* #caption "generation lemma for lift" *)
 (*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
 
       Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
                              (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
-
-(*#* #stop file *)
-
       Intros until 1; InsertEq H '(lift h d t1);
       UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
       Rename x into t3; Rename x0 into d.
@@ -66,7 +61,7 @@ Require pr0_lift.
       LiftGen; Rewrite H3; Clear H3 t0.
       LiftGen; Rewrite H3; Clear H3 H5 x1 k.
       IH; IH; XEAuto.
-(* case 4 : pr0_gamma *)
+(* case 4 : pr0_upsilon *)
       LiftGen; Rewrite H6; Clear H6 t0.
       LiftGen; Rewrite H6; Clear H6 x1.
       IH; IH; IH.