diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 13:10:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 13:10:18 +0200 |
| commit | c3ce76de37a988c120654760629b4609272f8885 (patch) | |
| tree | 8ad851468b3d0b9fb3bfd775f4c760af97c560f8 /pretyping/typing.mli | |
| parent | 79220cec31a9c2c5cafc678b36f7af374417ecd5 (diff) | |
Refresh universes for Ltac's type_of, as the term can be used anywhere,
fixing two opened bugs from HoTT/coq.
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 |