X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fdefndb.ma;h=69e0d400de84958a4ae682a99561cc831f8c84c2;hb=47a745462a714af9d65cea7b61af56524bd98fa1;hp=745090de4bb719b834c2c96f7424aab879c91d7a;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/POPLmark/Fsub/defndb.ma b/matita/matita/contribs/POPLmark/Fsub/defndb.ma
index 745090de4..69e0d400d 100644
--- a/matita/matita/contribs/POPLmark/Fsub/defndb.ma
+++ b/matita/matita/contribs/POPLmark/Fsub/defndb.ma
@@ -71,9 +71,9 @@ notation "hvbox(e ⊢ break ta ⊴  break tb)"
 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
 
 notation > "hvbox(\Forall S.T)" 
-  non associative with precedence 60 for @{ 'forall $S $T}.
+  non associative with precedence 65 for @{ 'forall $S $T}.
 notation < "hvbox('All' \sub S. break T)" 
-  non associative with precedence 60 for @{ 'forall $S $T}.
+  non associative with precedence 65 for @{ 'forall $S $T}.
 interpretation "universal type" 'forall S T = (Forall S T).
   
 notation "#x" with precedence 79 for @{'tvar $x}.
@@ -83,11 +83,11 @@ notation "⊤" with precedence 90 for @{'toptype}.
 interpretation "toptype" 'toptype = Top.
 
 notation "hvbox(s break ⇛ t)"
-  right associative with precedence 55 for @{ 'arrow $s $t }.
+  right associative with precedence 60 for @{ 'arrow $s $t }.
 interpretation "arrow type" 'arrow S T = (Arrow S T).
 
 notation "hvbox(⊴ T)"
-  non associative with precedence 60 for @{ 'subtypebound $T }.
+  non associative with precedence 65 for @{ 'subtypebound $T }.
 interpretation "subtyping bound" 'subtypebound T = (mk_bound true T).  
 
 (****** PROOFS ********)