ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v
index e092e23e7eef11578a4601c7db6290b6b04ef2e3..9f9b6da8655c2f45bc9d96d8807370b657624dca 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v
@@ -21,7 +21,7 @@ Require subst0_lift.
                              (u1,u:?; i:?) (subst0 i u u1 u2) ->
                              (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
       Intros until 1; XElim H; Intros.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
       Arith5 i0 i; XEAuto.
 (* case 2 : subst0_fst *)
       IH; XEAuto.
@@ -35,7 +35,7 @@ Require subst0_lift.
                                   (u1,u:?; i:?) (subst0 i u u2 u1) ->
                                   (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
       Intros until 1; XElim H; Intros.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
       Arith5 i0 i; XEAuto.
 (* case 2 : subst0_fst *)
       IH; XEAuto.