Merge branch 'v8.6'

2 files changed, 20 insertions, 2 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index d8a658e3e3..bffb407274 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -854,6 +854,13 @@ let is_eq_sort s1 s2 =
       if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
+(* Precondition: l is not defined in the substitution *)
+let universe_rigidity evd l =
+  let uctx = evd.universes in
+  if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then
+    UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx))
+  else UnivRigid
+
 let normalize_universe evd =
   let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
diff --git a/engine/evd.mli b/engine/evd.mli
index 5c9effd4be..993ed300bc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map
 (*********************************************************
    Sort/universe variables *)
 
-(** Rigid or flexible universe variables *)
+(** Rigid or flexible universe variables.
+
+   [UnivRigid] variables are user-provided or come from an explicit
+   [Type] in the source, we do not minimize them or unify them eagerly.
+
+   [UnivFlexible alg] variables are fresh universe variables of
+   polymorphic constants or generated during refinement, sometimes in
+   algebraic position (i.e. not appearing in the term at the moment of
+   creation). They are the candidates for minimization (if alg, to an
+   algebraic universe) and unified eagerly in the first-order
+   unification heurstic.  *)
 
 type rigid = UState.rigid =
   | UnivRigid
@@ -514,7 +524,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
 val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
-											   
+
+val universe_rigidity : evar_map -> Univ.Level.t -> rigid
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is