diff options
| author | Matthieu Sozeau | 2015-11-05 16:04:43 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-11 19:13:52 +0100 |
| commit | 2f56f0fcf21902bb1317f1d6f7ba4b593d712646 (patch) | |
| tree | 66ac9f8f8e35cf2146b8e5f8bb02ec72c6c5f575 /pretyping/evarsolve.ml | |
| parent | 701a69732ef2abfc7384296e090a3e9bd7604bbd (diff) | |
Fix bug #4293: ensure let-ins do not contain algebraic universes in
their type annotation.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 35bc1de593..aeb2445d1c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,7 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -98,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = if isArity t then (match pbty with | None -> t - | Some dir -> refresh univ_rigid dir t) + | Some dir -> refresh status dir t) else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -609,7 +609,8 @@ 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 ~inferred:true (Some false) env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes + ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in let evd,b_in_sign = match b with @@ -627,7 +628,8 @@ 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 ~inferred:true (Some false) env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes + ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd,ev2_in_sign = |