X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fsubst0_subst0.v;h=9f9b6da8655c2f45bc9d96d8807370b657624dca;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e092e23e7eef11578a4601c7db6290b6b04ef2e3;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v
index e092e23e7..9f9b6da86 100644
--- 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.