X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fgrammar%2Flenv_length.ma;h=23e445907c470d50552ed028fea54aa295450ed0;hb=cd0870e2572a77bd69bda4b8c403c30b569c58b9;hp=437730a83301baef415e65a4d77c1bc982d051e5;hpb=fd991956035d0f1b663aab48325097e53ed9e00e;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
index 437730a83..23e445907 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma
@@ -14,11 +14,10 @@
 
 include "Basic-2/grammar/lenv.ma".
 
-(* LENGTH *******************************************************************)
+(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
 
-(* the length of a local environment *)
 let rec length L ≝ match L with
-[ LSort       ⇒ 0
+[ LAtom       ⇒ 0
 | LPair L _ _ ⇒ length L + 1
 ].