diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 6 | ||||
| -rw-r--r-- | pretyping/typing.mli | 5 |
2 files changed, 7 insertions, 4 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5cd05c58d6..2f34f7efea 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -285,11 +285,13 @@ let sort_of env evd c = (* Try to solve the existential variables by typing *) -let e_type_of env evd c = +let e_type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) - !evdref, j.uj_type + if refresh then + Evarsolve.refresh_universes false !evdref j.uj_type + else !evdref, j.uj_type let solve_evars env evdref c = let c = (execute env evdref c).uj_val in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8b194a9c9a..26dc8c560e 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 |