...

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index c386743e74f466edcf5bff9938d9d9142b6de1de..448217888125fc515b0e37e42c49bf641789d9f7 100644 (file)
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/matita/tests/coercions_russell.ma
@@ -101,8 +101,8 @@ simplify; apply (eqb_elim x hd); simplify; intros;
 simplify; autobatch;
 qed.
 
-notation > "'If' b 'Then' t 'Else' f" 
-for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
+notation > "'If' b 'Then' t 'Else' f" non associative
+with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
 
 definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
 (* define the find function *)