X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fi_static%2Ftc_lfxs.ma;h=5fbe3afe2a6ec8e13cc2867d052a77c1d20eafa5;hb=75f395f0febd02de8e0f881d918a8812b1425c8d;hp=90b0de1eb649fc618778637ded5582e583777f64;hpb=d59f344b1e4b377e2f06abd9f8856d686d21b222;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma
index 90b0de1eb..5fbe3afe2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma
@@ -18,7 +18,7 @@ include "basic_2/static/lfxs.ma".
 
 (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
 
-definition tc_lfxs (R): term → relation lenv ≝ LTC … (lfxs R).
+definition tc_lfxs (R): term → relation lenv ≝ CTC … (lfxs R).
 
 interpretation "iterated extension on referred entries (local environment)"
    'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2).