- 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 2321e7b0d760da23e4cb2adf0ce86ab4983da3ea..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
@@ -17,7 +17,7 @@ include "Basic-2/grammar/lenv.ma".
 (* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
 
 let rec length L ≝ match L with
-[ LSort       ⇒ 0
+[ LAtom       ⇒ 0
 | LPair L _ _ ⇒ length L + 1
 ].