update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / genv_length.ma

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 15244609af5af016dbde569c9bb02d0ce25b4dc1..bda7b391e767c9b2b9a04a8be5ac859cfb11b172 100644 (file)
--- 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)"