...

[helm.git] / helm / software / matita / nlibrary / re / re.ma

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 2899fbc186e7a602405856a6be8f2f853de6658f..c66c73791e7304b155a152e3463843dcf2b7b08d 100644 (file)
--- 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}.