diff options
| author | Matthieu Sozeau | 2014-06-21 16:14:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-21 16:14:59 +0200 |
| commit | 14ae5f4534ee5e632d82990e7db76305b9ca9b75 (patch) | |
| tree | 7ba63a0f2de145d04dddf01e17e25beeebbc72f6 /pretyping | |
| parent | 9b3a234e4cf002292ca4a67e1b72daac463b4c46 (diff) | |
- Add an option to refresh only algebraic universes, for e_type_of. The goal
there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 3 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 26e96af48b..9522f9c249 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,7 +42,7 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_universes dir env evd t = +let refresh_universes ?(onlyalg=false) dir env evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = @@ -50,7 +50,7 @@ let refresh_universes dir env evd t = | Sort (Type u as s) when (match Univ.universe_level u with | None -> true - | Some l -> Option.is_empty (Evd.is_sort_variable evd s)) -> + | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) -> (* s' will appear in the term, it can't be algebraic *) let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in let evd = diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 988938272a..6de8f5c8dc 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,7 +34,8 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : bool (* direction: true for levels lower than the existing levels *) -> +val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> + bool (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7702355b8c..1c41a5bb3a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes false env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = |