X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fre%2Fre.ma;h=c66c73791e7304b155a152e3463843dcf2b7b08d;hb=a8ae2efbf7e09d6ddbb1eb9fd79cafa4e045ff9a;hp=2899fbc186e7a602405856a6be8f2f853de6658f;hpb=e678e3b1a88e657401902bbddad02d3a4d70205a;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 2899fbc18..c66c73791 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -125,17 +125,17 @@ interpretation "patom" 'ps a = (ps ? a).
 interpretation "pepsilon" 'epsilon = (pe ?).
 interpretation "pempty" 'empty = (pz ?).
 
-notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
+notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
  match l with
   [ pz ⇒ ∅
   | pe ⇒ ϵ
   | ps x ⇒ `x
   | pp x ⇒ `x
-  | pc E1 E2 ⇒ (.|E1| · .|E2|)
-  | po E1 E2 ⇒ (.|E1| + .|E2|)
-  | pk E ⇒ .|E|^* ].
-notation < ".|term 19 e|" non associative with precedence 90 for @{'forget $e}.
+  | pc E1 E2 ⇒ (|E1| · |E2|)
+  | po E1 E2 ⇒ (|E1| + |E2|)
+  | pk E ⇒ |E|^* ].
+notation < ".|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 interpretation "forget" 'forget a = (forget ? a).
 
 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.