diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /pretyping/typing.mli | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
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 1f822f1a..bfae46ff 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 |