From 14ae5f4534ee5e632d82990e7db76305b9ca9b75 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 21 Jun 2014 16:14:59 +0200 Subject: - 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. --- pretyping/evarsolve.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/evarsolve.ml') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 26e96af48..9522f9c24 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 = -- cgit v1.2.3