X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fgenv_length.ma;h=bda7b391e767c9b2b9a04a8be5ac859cfb11b172;hp=15244609af5af016dbde569c9bb02d0ce25b4dc1;hb=222044da28742b24584549ba86b1805a87def070;hpb=3c8da07d7a5d7cf0432a83732a6d103f527afaef

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
index 15244609a..bda7b391e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
@@ -18,7 +18,7 @@ include "basic_2/syntax/genv.ma".
 
 rec definition glength G on G ≝ match G with
 [ GAtom       ⇒ 0
-| GBind G _ _ ⇒ ↑(glength G)
+| GPair G _ _ ⇒ ↑(glength G)
 ].
 
 interpretation "length (global environment)"