pair => mk_Prod (one more was left in notation)

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 697cf10a4c309216791e30b2aba32f8caa2714cf..060ebb06e84844c5582af4b89b37fb581f7d0ea1 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -109,7 +109,7 @@ for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh
 
 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
  with precedence 10
-for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
+for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
 
 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
  with precedence 10