X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2FPTS%2Fgpts.ma;fp=matita%2Fmatita%2Fnlibrary%2FPTS%2Fgpts.ma;h=d866087a8bd5560ea60144ca5412d0ecc3d09df1;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=9af90225239158d425d63dd8cd90d8b2fbc2b1a7;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git

diff --git a/matita/matita/nlibrary/PTS/gpts.ma b/matita/matita/nlibrary/PTS/gpts.ma
index 9af902252..d866087a8 100644
--- a/matita/matita/nlibrary/PTS/gpts.ma
+++ b/matita/matita/nlibrary/PTS/gpts.ma
@@ -52,7 +52,7 @@ ninductive TJ: list T → T → T → Prop ≝
   | conv: ∀G.∀A,B,C.∀i. conv B C →
      TJ G A B → TJ G B (Sort i) → TJ G A C.
      
-notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+notation "hvbox(G break  ⊢ A : B)" non associative with precedence 55 for @{'TJ $G $A $B}.
 interpretation "type judgement" 'TJ G A B = (TJ G A B).
 
 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)