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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
index 87bf9c8c0..b5fef207b 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
@@ -11,7 +11,7 @@ Require subst0_defs.
                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                  (le (weight_map f z) (weight_map g t)).
       Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
       Intros; XAuto.
 (* case 2: subst0_fst *)
       XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
@@ -26,7 +26,7 @@ Require subst0_defs.
                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                  (lt (weight_map f z) (weight_map g t)).
       Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
       Intros; XAuto.
 (* case 2: subst0_fst *)
       XElim k; [ XElim b | Idtac ]; Simpl; Intros;