From 95a4fcf8cd36e29034e886682ed3a6e2914ce04f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Nov 2015 12:52:35 -0500
Subject: 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.
---
 pretyping/evarsolve.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3c3720388f..ee666e1154 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'
-- 
cgit v1.2.3