X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flibrary%2Fnat%2Fpi_p.ma;h=cf7969841aa4c75654d992781ad4ba2bc9b0415d;hb=HEAD;hp=b526e8d51be947dd7cc114340b6ccf75da4ee765;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/library/nat/pi_p.ma b/matita/matita/library/nat/pi_p.ma
index b526e8d51..cf7969841 100644
--- a/matita/matita/library/nat/pi_p.ma
+++ b/matita/matita/library/nat/pi_p.ma
@@ -29,28 +29,28 @@ notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­
             (p
             \atop 
             (ident i < n)) f" 
-non associative with precedence 60 for 
+non associative with precedence 65 for 
 @{ 'product $n (λ${ident i}:$xx1.$p) (λ${ident i}:$xx2.$f) }.
 
 notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Π) ­
              ) 
             \below 
             ((ident i < n)) f" 
-non associative with precedence 60 for 
+non associative with precedence 65 for 
 @{ 'product $n (λ_:$xx1.$xx3) (λ${ident i}:$xx2.$f) }.
 
 interpretation "big product" 'product n p f = (pi_p n p f).
 
 notation > "'Pi' (ident x) < n | p . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
 for @{ 'product $n (λ${ident x}.$p) (λ${ident x}.$f) }. 
 
 notation > "'Pi' (ident x) ≤ n | p . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
 for @{ 'product (S $n) (λ${ident x}.$p) (λ${ident x}.$f) }. 
 
 notation > "'Pi' (ident x) < n . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
 for @{ 'product $n (λ_.true) (λ${ident x}.$f) }. 
 *)