X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=b7a022ad201056d7d5d1842ea9b3def64d0d862b;hb=913512bbc9202f2109d53acd43dc8c0270b17184;hp=1dcd79b7a49892702ba1290f86f3cb0099d3e335;hpb=179aad29c98fcb78c8859e8a044e342b9259dd02;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 1dcd79b7a..b7a022ad2 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -145,10 +145,10 @@ for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} 
        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
         λ${ident E}.$s ] ] (refl ? $t) }.
 
-notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp 'as' \nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
-for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
-       match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → $U with [ mk_Prod (${ident xy}:$V) (${ident z}:$Z) ⇒
+       match $xy return λ${ident a}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
         λ${ident E}:$J.$s ] ] ($refl $A $t) }.
 
 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"