From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Apr 2009 12:21:54 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4070
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4446f96e1829f1a82fc71cb49d8ddc392e73b155;p=helm.git

...
---

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index c386743e7..448217888 100644
--- 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 *)