diff options
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 63fb0679f1..1b07b2bb78 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -57,3 +57,4 @@ val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment val judge_of_int : Environ.env -> Uint63.t -> unsafe_judgment +val judge_of_float : Environ.env -> Float64.t -> unsafe_judgment |