ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
index 9f828bfa8a014b4f6d7c5b92a6e54ff9d4d35baf..3546cb5f2caa52a2a49d5a3b5db8f256ec10229e 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v
@@ -1,3 +1,5 @@
+(*#* #stop file *)
+
 Require subst0_lift.
 Require drop_props.
 Require pr0_lift.
@@ -14,11 +16,8 @@ Require pr2_defs.
       Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
                          (t1,t2:?) (pr2 e t1 t2) ->
                          (pr2 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
       Intros until 2; XElim H0; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
       XAuto.
 (* case 2 : pr2_delta *)
       Apply (lt_le_e i d); Intros; DropDis.