update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_static / tc_lfxs.ma

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 90b0de1eb649fc618778637ded5582e583777f64..5fbe3afe2a6ec8e13cc2867d052a77c1d20eafa5 100644 (file)
--- 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).