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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
index 689477a39..eb3f6fb27 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
@@ -7,7 +7,7 @@ Require Export terms_defs.
 
       Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
          | (TSort n)               => (0)
-         | (TBRef n)               => (f n)
+         | (TLRef n)               => (f n)
          | (TTail (Bind Abbr) u t) =>
             (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
          | (TTail (Bind _) u t)    =>