diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 12:52:35 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 12:52:35 -0500 |
| commit | 95a4fcf8cd36e29034e886682ed3a6e2914ce04f (patch) | |
| tree | 408edac97bef6e69ab3503500a1220015110db52 | |
| parent | b30ca8ac9e0225e6505fea0004ea37e7649c9cb6 (diff) | |
Univs: compatibility with 8.4.
When refreshing a type variable, always use a rigid universe to force the most
general universe constraint, as in 8.4.
| -rw-r--r-- | pretyping/evarsolve.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3c3720388..ee666e115 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,10 +42,6 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let default_universe_status u = - if Flags.version_less_or_equal Flags.V8_4 then univ_rigid - else u - let refresh_level evd s = match Evd.is_sort_variable evd s with | None -> true @@ -60,8 +56,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = (match Univ.universe_level u with | None -> true | Some l -> not onlyalg && refresh_level evd s) -> - let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in - let s' = evd_comb0 (new_sort_variable (default_universe_status status)) evdref in + let s' = evd_comb0 (new_sort_variable univ_rigid) evdref in let evd = if dir then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' |