better, reparsable, notation

[helm.git] / helm / software / matita / core_notation.moo

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index c6e3d6015c61ef563ef48f0daf02c18a2a48cbbc..9055293175f66328f4719569dfa7d1c142ecdc74 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -10,14 +10,14 @@ with precedence 90 for @{ 'pair $a $b}.
 notation "hvbox(x break \times y)" with precedence 70
 for @{ 'product $x $y}.
 
-notation < "\fst \nbsp x" non associative with precedence 69 for @{'pi1a $x}.
-notation < "\snd \nbsp x" non associative with precedence 69 for @{'pi2a $x}.
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
 
-notation < "\fst \nbsp x \nbsp y" non associative with precedence 69 for @{'pi1b $x $y}.
-notation < "\snd \nbsp x \nbsp y" non associative with precedence 69 for @{'pi2b $x $y}.
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
 
-notation > "\fst" non associative with precedence 90 for @{'pi1}.
-notation > "\snd" non associative with precedence 90 for @{'pi2}.
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
 
 notation "hvbox(a break \to b)" 
   right associative with precedence 20