- notation fixed according to the new stricter semantics

[helm.git] / helm / software / matita / contribs / dama / dama / cprop_connectives.ma

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 9e0e4b5fbb8e19c245c707d29f931923e91f2579..aabf6e79e08906331e8883e659a79f6c5ac19f6c 100644 (file)
--- 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).