diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index c71a0e0ca4..ae816fe26e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -120,6 +120,9 @@ val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit val type_of_int : env -> types val judge_of_int : env -> Uint63.t -> unsafe_judgment +val type_of_float : env -> types +val judge_of_float : env -> Float64.t -> unsafe_judgment + val type_of_prim_type : env -> CPrimitives.prim_type -> types val type_of_prim : env -> CPrimitives.t -> types |