arith.ml.patch

1593c1593
<     ASM_METIS_TAC[DIVISION; MULT_SYM];
---
>     ASM_MESON_TAC[DIVISION; MULT_SYM]; (* OA: Metis *)
1696c1696
<   let MOD_SUC_MOD = METIS[ADD1; MOD_ADD_MOD; MOD_MOD_REFL]
---
>   let MOD_SUC_MOD = MESON[ADD1; MOD_ADD_MOD; MOD_MOD_REFL] (* OA: Metis *)
1705c1705
<   and upconv =
---
>   and upconv tm =
1707c1707
<      [MOD_SUC_MOD; MOD_ADD_MOD; MOD_MULT_MOD2; MOD_EXP_MOD; MOD_MOD_REFL] in
---
>      [MOD_SUC_MOD; MOD_ADD_MOD; MOD_MULT_MOD2; MOD_EXP_MOD; MOD_MOD_REFL] tm in
1720c1720
<     else if h1 < h2 then minter i (h1::l1') l2' (tl l1) l2
---
>     else if Term.(<) h1 h2 then minter i (h1::l1') l2' (tl l1) l2
1729,1730c1729,1730
<     let lats = sort (<=) (binops `(+)` l)
<     and rats = sort (<=) (binops `(+)` r) in
---
>     let lats = sort Term.(<) (binops `(+)` l)
>     and rats = sort Term.(<) (binops `(+)` r) in
1859c1859
< let BITS_ELIM_CONV : conv =
---
> let (BITS_ELIM_CONV : conv) =
1870,1871c1870,1871
<   let rec BITS_ELIM_CONV : conv =
<     fun tm -> match tm with
---
>   let rec BITS_ELIM_CONV tm =
>     match tm with