X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=909231ae809d6d26115076fce5818b00bb83da8d;hb=784a534f6d969a261f45396307d0ef30f7fb2be2;hp=a15c5309b9b3308daae7f84e35b158d67e8a9296;hpb=7ed62d94780c881c3ee056418b00ad5e9f739f15;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index a15c5309b..909231ae8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -29,7 +29,7 @@ inductive lenv: Type[0] ≝
 interpretation "sort (local environment)"
    'Star = LAtom.
 
-interpretation "environment binding construction (binary)"
+interpretation "local environment binding construction (binary)"
    'DxBind2 L I T = (LPair L I T).
 
 interpretation "abbreviation (local environment)"