X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fcprop_connectives.ma;h=aabf6e79e08906331e8883e659a79f6c5ac19f6c;hb=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;hp=9e0e4b5fbb8e19c245c707d29f931923e91f2579;hpb=813f73e76fb7374987ea1e826bcd6f15e22377d9;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 9e0e4b5fb..aabf6e79e 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -28,14 +28,14 @@ interpretation "constructive and" 'and x y = (And x y).
 inductive And3 (A,B,C:CProp) : CProp ≝
  | Conj3 : A → B → C → And3 A B C.
 
-notation < "a ∧ b ∧ c" left associative with precedence 35 for @{'and3 $a $b $c}.
+notation < "a ∧ b ∧ c" with precedence 35 for @{'and3 $a $b $c}.
  
 interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
 
 inductive And4 (A,B,C,D:CProp) : CProp ≝
  | Conj4 : A → B → C → D → And4 A B C D.
 
-notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4 $a $b $c $d}.
+notation < "a ∧ b ∧ c ∧ d" with precedence 35 for @{'and4 $a $b $c $d}.
  
 interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).