ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / tlt_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v
index 689477a39f3332a879f5d1131e9a85c2d50563e7..eb3f6fb27a5f40a5996ceff337d57753bb466909 100644 (file)
--- 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)    =>