X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Fmoves.ma;h=5825317771ee6f5672b92d25cd97713166d048bd;hb=eaaea3c18083de3e442e939768ff450d3b093911;hp=1372b49760ee677eea226d73a3a70392bc869e86;hpb=dc66c8d89a5147178ccdacb8341ed26c9c52f06b;p=helm.git diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index 1372b4976..582531777 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -110,7 +110,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