- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / nlibrary / PTS / gpts.ma

diff --git a/matita/matita/nlibrary/PTS/gpts.ma b/matita/matita/nlibrary/PTS/gpts.ma
index 9af90225239158d425d63dd8cd90d8b2fbc2b1a7..d866087a8bd5560ea60144ca5412d0ecc3d09df1 100644 (file)
--- 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. *)