diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 22 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 2 |
2 files changed, 12 insertions, 12 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5f19ce30a6..08b704bdea 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,7 @@ let get_polymorphic_positions f = hd ?A (l : list t) -> A = t *) -let refresh_universes ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = @@ -56,15 +56,15 @@ let refresh_universes ?(onlyalg=false) pbty env evd t = (match Univ.universe_level u with | None -> true | 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 = - if dir then set_leq_sort !evdref s' s - else set_leq_sort !evdref s s' - in - modified := true; evdref := evd; mkSort s' + let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = + if dir then set_leq_sort !evdref s' s + else set_leq_sort !evdref s s' + in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars t = @@ -561,7 +561,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let id = next_name_away na avoid in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in - let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd t_in_env ty_t_in_sign sign filter inst_in_env in let evd,b_in_sign = match b with @@ -580,7 +580,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in - let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes ~inferred:true (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd,ev2_in_sign = diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 16a4aff5bf..e35fb44b15 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,7 +34,7 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : ?inferred:bool -> ?onlyalg:bool (* Only algebraic universes *) -> bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types |