- the theory of parallel substitution of local environments (ltps) is ready

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / grammar / lenv_length.ma

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 437730a83301baef415e65a4d77c1bc982d051e5..23e445907c470d50552ed028fea54aa295450ed0 100644 (file)
--- 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
 ].