diff options
| author | Matthieu Sozeau | 2014-05-09 13:10:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-09 13:10:18 +0200 |
| commit | c3ce76de37a988c120654760629b4609272f8885 (patch) | |
| tree | 8ad851468b3d0b9fb3bfd775f4c760af97c560f8 /pretyping | |
| 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')
| -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 |