bug fix in notation precedences

[helm.git] / matita / matita / contribs / lambda / delifting_substitution.ma

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index 6e648c9a890969adb44c14ad433b247986d174a6..344ad849021c3fc088440dc7c2b7fcc308870621 100644 (file)
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -27,12 +27,12 @@ interpretation "delifting substitution"
    'DSubst C d M = (dsubst C d M).
 
 (* Note: the notation with "/" does not work *)
-notation "hvbox( [ d ⬐ break C ] break term 55 M )"
-   non associative with precedence 55
+notation "hvbox( [ term 46 d ⬐ break term 46 C ] break term 46 M )"
+   non associative with precedence 46
    for @{ 'DSubst $C $d $M }.
 
-notation > "hvbox( [ ⬐ C ] break term 55 M )"
-   non associative with precedence 55
+notation > "hvbox( [ ⬐ term 46 C ] break term 46 M )"
+   non associative with precedence 46
    for @{ 'DSubst $C 0 $M }.
 
 lemma dsubst_vref_lt: ∀i,d,C. i < d → [d ⬐ C] #i = #i.