X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fre_complete%2Fmoves.ma;h=a14487498a9accfc5227bcf9579ad1c2282c4c55;hb=12d58352dbd62df65d44becc0f69fc5a7b370866;hp=dc7474e21c42c2cfcc951ede34655b4699d1fe0c;hpb=0d481cc22ba8ada5781885da5398086a0b5662f3;p=helm.git diff --git a/matita/matita/re_complete/moves.ma b/matita/matita/re_complete/moves.ma index dc7474e21..a14487498 100644 --- a/matita/matita/re_complete/moves.ma +++ b/matita/matita/re_complete/moves.ma @@ -68,7 +68,7 @@ theorem move_ok: ] qed. -notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. +notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}. let rec moves (S : DeqSet) w e on w : pre S ≝ match w with [ nil ⇒ e