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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_props.v b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v
index 5d5d7d0a9..366ad999b 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v
@@ -9,12 +9,12 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Repeat Rewrite lift_bref_lt; XEAuto.
+      Repeat Rewrite lift_lref_lt; XEAuto.
 (* case 2.2: n >= d *)
-      Repeat Rewrite lift_bref_ge; XEAuto.
+      Repeat Rewrite lift_lref_ge; XEAuto.
 (* case 3: TTail k *)
       LiftTailRw; XAuto.
       Qed.
@@ -24,18 +24,18 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n e); Intros.
 (* case 2.1: n < e *)
-      Cut (lt n d); Intros; Repeat Rewrite lift_bref_lt; XEAuto.
+      Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
 (* case 2.2: n >= e *)
-      Rewrite lift_bref_ge; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge; [ Idtac | XAuto ].
       Rewrite plus_sym; Apply (lt_le_e n d); Intros.
 (* case 2.2.1: n < d *)
-      Do 2 (Rewrite lift_bref_lt; [ Idtac | XAuto ]).
-      Rewrite lift_bref_ge; XAuto.
+      Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
+      Rewrite lift_lref_ge; XAuto.
 (* case 2.2.2: n >= d *)
-      Repeat Rewrite lift_bref_ge; XAuto.
+      Repeat Rewrite lift_lref_ge; XAuto.
 (* case 3: TTail k *)
       LiftTailRw; SRw; XAuto.
       Qed.