X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_bars.ma;h=ef16cd2bc800af6d0d11b386332a28a6d41abf5c;hb=85a42e4a2a4c62818b6a98eff545e58ceb8770a4;hp=2cad9ca2add1adbdb9efa018723ee99809c4b99f;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/contribs/dama/dama/models/q_bars.ma b/matita/matita/contribs/dama/dama/models/q_bars.ma
index 2cad9ca2a..ef16cd2bc 100644
--- a/matita/matita/contribs/dama/dama/models/q_bars.ma
+++ b/matita/matita/contribs/dama/dama/models/q_bars.ma
@@ -196,6 +196,6 @@ cases (?:False);
 [ apply (q_lt_corefl ? H)| cases (q_lt_le_incompat ?? (q_neg_gt ?) (q_lt_to_le ?? H))]
 qed.
 
-notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
+notation < "x \blacksquare" non associative with precedence 55 for @{'unpos $x}.
 interpretation "hide unpos proof" 'unpos x = (unpos x ?).