diff options
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f822f1a5..bfae46ff8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -13,12 +13,15 @@ open Evd (** This module provides the typing machine with existential variables and universes. *) -(** Typecheck a term and return its type *) -val type_of : env -> evar_map -> constr -> types +(** Typecheck a term and return its type. May trigger an evarmap leak. *) +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types + +(** Variant of [type_of] using references instead of state-passing. *) +val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) val sort_of : env -> evar_map ref -> types -> sorts |