context-free parallel reduction on closures is confluent!

[helm.git] / matita / matita / contribs / dama / dama / models / q_bars.ma

diff --git a/matita/matita/contribs/dama/dama/models/q_bars.ma b/matita/matita/contribs/dama/dama/models/q_bars.ma
index 2cad9ca2add1adbdb9efa018723ee99809c4b99f..ef16cd2bc800af6d0d11b386332a28a6d41abf5c 100644 (file)
--- 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 ?).