- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / re_complete / lang.ma

diff --git a/matita/matita/re_complete/lang.ma b/matita/matita/re_complete/lang.ma
index 430fc3f2140b002580629e498d0a89762b2a808d..510d2215c02803ec2efce63bf4352e45210d2075 100644 (file)
--- a/matita/matita/re_complete/lang.ma
+++ b/matita/matita/re_complete/lang.ma
@@ -10,7 +10,7 @@ interpretation "epsilon" 'epsilon = (nil ?).
 (* concatenation *)
 definition cat : ∀S,l1,l2,w.Prop ≝ 
   λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
 
 let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝