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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
index 3a9cb3fce..7319f3264 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
@@ -17,12 +17,12 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt; XAuto.
+      Rewrite lift_lref_lt; XAuto.
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge; [ Simpl | XAuto ].
+      Rewrite lift_lref_ge; [ Simpl | XAuto ].
       Rewrite (H n); XAuto.
 (* case 3: TTail k *)
       XElim k; Intros; LiftTailRw; Simpl.
@@ -48,12 +48,12 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       XAuto.
-(* case 2: TBRef *)
+(* case 2: TLRef *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Repeat Rewrite lift_bref_lt; Simpl; XAuto.
+      Repeat Rewrite lift_lref_lt; Simpl; XAuto.
 (* case 2.2: n >= d *)
-      Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
+      Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
 (* case 3: TTail k *)
       XElim k; Intros; LiftTailRw; Simpl.
 (* case 1 : bind b *)
@@ -84,6 +84,4 @@ Require lift_defs.
 
       Hints Resolve lift_tlt_dx : ltlc.
 
-(*#* #start file *)
-
 (*#* #single *)