X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fdefn.ma;h=4e48e27de62eadd62e455f82a73fca73f50ccc52;hb=325bc2fb36e8f8db99a152037d71332c9ac7eff9;hp=337fe26868c6f5663c82aa943f779aa16060d6a2;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/POPLmark/Fsub/defn.ma b/matita/matita/contribs/POPLmark/Fsub/defn.ma
index 337fe2686..4e48e27de 100644
--- a/matita/matita/contribs/POPLmark/Fsub/defn.ma
+++ b/matita/matita/contribs/POPLmark/Fsub/defn.ma
@@ -108,9 +108,9 @@ notation "mstyle color #007f00 (hvbox(e ⊢ break t))"
 interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
 
 notation > "\Forall S.T" 
-  non associative with precedence 60 for @{ 'forall $S $T}.
+  non associative with precedence 65 for @{ 'forall $S $T}.
 notation < "hvbox(⊓ \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}.
@@ -123,7 +123,7 @@ 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(S [#n ↦ T])"
@@ -131,7 +131,7 @@ notation "hvbox(S [#n ↦ T])"
 interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).  
 
 notation "hvbox(!X ⊴ T)"
-  non associative with precedence 60 for @{ 'subtypebound $X $T }.
+  non associative with precedence 65 for @{ 'subtypebound $X $T }.
 interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T).  
 
 (****** PROOFS ********)