Первый раз наткнулся на ошибку в ocaml

Причем свежевставленную: в 4.05.0:

В Why3 в core/term.mli:

val t_const : Number.constant -> term

в core/term.ml:

let t_const c ty = mk_term (Tconst c) (Some ty)
...
let t_const c = match c with
| Number.ConstInt _ -> t_const c ty_int
| Number.ConstReal _ -> t_const c ty_real

В результате экспортится первое из определений t_const, причем с типом:

Number.constant -> Ty.ty -> term

Что интересно - на простом примере не воспроизводится