diff options
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8b194a9c9..26dc8c560 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -17,8 +17,9 @@ open Evd (** Typecheck a term and return its type *) val type_of : env -> evar_map -> constr -> types -(** Typecheck a term and return its type + updated evars *) -val e_type_of : env -> evar_map -> constr -> evar_map * 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 (** Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> sorts |