Split off Universes functions about substitutions and constraints

16 files changed, 640 insertions, 460 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index d30cb74d7..2ab545612 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -446,28 +446,28 @@ let compare_constr sigma cmp c1 c2 =
   compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
-  let open Universes in
+  let open UnivProblem in
   if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
   else
     CArray.fold_left3
       (fun cstrs v u u' ->
          let open Univ.Variance in
          match v with
-         | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs
+         | Irrelevant -> Set.add (UWeak (u,u')) cstrs
          | Covariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
            (match cv_pb with
-            | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
-            | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+            | Reduction.CONV -> Set.add (UEq (u,u')) cstrs
+            | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs)
          | Invariant ->
            let u = Univ.Universe.make u in
            let u' = Univ.Universe.make u' in
-           Constraints.add (UEq (u,u')) cstrs)
+           Set.add (UEq (u,u')) cstrs)
       cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
@@ -480,7 +480,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
     compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
-  let open Universes in
+  let open UnivProblem in
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     cstrs
@@ -491,7 +491,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
-      Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs))
+      Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
         cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
 
 let eq_universes env sigma cstrs cv_pb ref nargs l l' =
@@ -499,8 +499,8 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
   else
     let l = Evd.normalize_universe_instance sigma l
     and l' = Evd.normalize_universe_instance sigma l' in
-    let open Universes in
     let open GlobRef in
+    let open UnivProblem in
     match ref with
     | VarRef _ -> assert false (* variables don't have instances *)
     | ConstRef _ ->
@@ -515,11 +515,11 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
       true
 
 let test_constr_universes env sigma leq m n =
-  let open Universes in
+  let open UnivProblem in
   let kind c = kind_upto sigma c in
-  if m == n then Some Constraints.empty
+  if m == n then Some Set.empty
   else
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
     let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
     and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
@@ -527,7 +527,7 @@ let test_constr_universes env sigma leq m n =
       let s1 = ESorts.kind sigma (ESorts.make s1) in
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
-      else (cstrs := Constraints.add 
+      else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
@@ -536,7 +536,7 @@ let test_constr_universes env sigma leq m n =
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
       else 
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
@@ -574,15 +574,15 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
-  let open Universes in
-  if m == n then Some Constraints.empty
+  let open UnivProblem in
+  if m == n then Some Set.empty
   else 
-    let cstrs = ref Constraints.empty in
+    let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
-	(cstrs := Constraints.add 
+        (cstrs := Set.add
            (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 743888a9b..b0e834b2e 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,11 +201,11 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
-val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
+val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 (** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)
-val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
 
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 512908e13..befd49dc9 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,5 +1,7 @@
 UnivNames
 UnivGen
+UnivSubst
+UnivProblem
 Universes
 Univops
 UState
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2b202ef3e..cb2d01bdf 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -86,7 +86,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
 let nf_evars_universes evm =
-  Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
+  UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm)
     (Evd.universe_subst evm)
     
 let nf_evars_and_universes evm =
@@ -830,13 +830,13 @@ let subterm_source evk ?where (loc,k) =
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
 let compare_cumulative_instances cv_pb variances u u' sigma =
-  let open Universes in
+  let open UnivProblem in
   let cstrs = Univ.Constraint.empty in
-  let soft = Constraints.empty in
+  let soft = Set.empty in
   let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
       let open Univ.Variance in
       match v with
-      | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft
+      | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft
       | Covariant when cv_pb == Reduction.CUMUL ->
         Univ.Constraint.add (u,Univ.Le,u') cstrs, soft
       | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
@@ -848,10 +848,10 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
   | exception Univ.UniverseInconsistency p -> Inr p
 
 let compare_constructor_instances evd u u' =
-  let open Universes in
+  let open UnivProblem in
   let soft =
-    Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs)
-      Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+    Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs)
+      Set.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
   in
   Evd.add_universe_constraints evd soft
 
@@ -870,7 +870,7 @@ let eq_constr_univs_test sigma1 sigma2 t u =
     with Univ.UniverseInconsistency _ | UniversesDiffer -> None
   in
   let ans =
-    Universes.eq_constr_univs_infer_with
+    UnivProblem.eq_constr_univs_infer_with
       (fun t -> kind_of_term_upto sigma1 t)
       (fun u -> kind_of_term_upto sigma2 u)
       (universes sigma2) fold t u sigma2
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 7dd98bac9..3ab2d3e34 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -284,5 +284,5 @@ val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 val e_new_global : evar_map ref -> GlobRef.t -> constr
 [@@ocaml.deprecated "Use [Evd.new_global]"]
 
-val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst
 [@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/engine/evd.ml b/engine/evd.ml
index b2b8e7ccc..03b843655 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -843,12 +843,12 @@ let universe_rigidity evd l =
 
 let normalize_universe evd =
   let vars = UState.subst evd.universes in
-  let normalize = Universes.normalize_universe_opt_subst vars in
+  let normalize = UnivSubst.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
   let vars = UState.subst evd.universes in
-  let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+  let normalize = UnivSubst.level_subst_of (UnivSubst.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
 let normalize_sort evars s =
@@ -866,7 +866,7 @@ let set_eq_sort env d s1 s2 =
   | Some (u1, u2) ->
     if not (type_in_type env) then
       add_universe_constraints d
-        (Universes.Constraints.singleton (Universes.UEq (u1,u2)))
+        (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2)))
     else
       d
 
@@ -878,7 +878,7 @@ let set_leq_level d u1 u2 =
 
 let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
-    (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
+    (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)
 
 let set_leq_sort env evd s1 s2 =
   let s1 = normalize_sort evd s1 
@@ -887,7 +887,7 @@ let set_leq_sort env evd s1 s2 =
   | None -> evd
   | Some (u1, u2) ->
      if not (type_in_type env) then
-       add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2)))
+       add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2)))
      else evd
 	    
 let check_eq evd s s' =
@@ -1297,7 +1297,7 @@ module MiniEConstr = struct
         | Some _ as v -> v
         | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
     in
-    Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
+    UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
 
   let of_named_decl d = d
   let unsafe_to_named_decl d = d
diff --git a/engine/evd.mli b/engine/evd.mli
index 7ce525744..b2670ee51 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -354,7 +354,7 @@ val whd_sort_variable : evar_map -> econstr -> econstr
 
 exception UniversesDiffer
 
-val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
+val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 (** Add the given universe unification constraints to the evar map.
     @raise UniversesDiffer in case a first-order unification fails.
     @raise UniverseInconsistency .
@@ -543,7 +543,7 @@ val empty_evar_universe_context : UState.t
 val union_evar_universe_context : UState.t -> UState.t ->
   UState.t
 [@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst
+val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst
 [@@ocaml.deprecated "Alias of UState.subst"]
 val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
 [@@ocaml.deprecated "Alias of UState.constrain_variables"]
@@ -603,7 +603,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
-val universe_subst : evar_map -> Universes.universe_opt_subst
+val universe_subst : evar_map -> UnivSubst.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
 (** [to_universe_context evm] extracts the local universes and
@@ -622,7 +622,7 @@ val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
 
 val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
-val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
+val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
 
 val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 9e975da58..c271d9d99 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -306,7 +306,7 @@ let pr_evar_universe_context ctx =
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-     h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+     h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
      str "WEAK CONSTRAINTS:"++brk(0,1)++
      h 0 (UState.pr_weak prl ctx) ++ fnl ())
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 839bb5ae9..6111ec7ed 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -27,7 +27,7 @@ type t =
  { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t;
    uctx_local : Univ.ContextSet.t; (** The local context of variables *)
    uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
-   uctx_univ_variables : Universes.universe_opt_subst;
+   uctx_univ_variables : UnivSubst.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.LSet.t; 
    (** The subset of unification variables that can be instantiated with
@@ -152,7 +152,8 @@ let drop_weak_constraints = ref false
 
 let process_universe_constraints ctx cstrs =
   let open Univ in
-  let open Universes in
+  let open UnivSubst in
+  let open UnivProblem in
   let univs = ctx.uctx_universes in
   let vars = ref ctx.uctx_univ_variables in
   let weak = ref ctx.uctx_weak_constraints in
@@ -203,7 +204,7 @@ let process_universe_constraints ctx cstrs =
   in
   let unify_universes cst local =
     let cst = nf_constraint cst in
-      if Constraints.is_trivial cst then local
+      if UnivProblem.is_trivial cst then local
       else 
           match cst with
           | ULe (l, r) ->
@@ -241,7 +242,7 @@ let process_universe_constraints ctx cstrs =
           | UEq (l, r) -> equalize_universes l r local
   in
   let local = 
-    Constraints.fold unify_universes cstrs Univ.Constraint.empty
+    UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty
   in
     !vars, !weak, local
 
@@ -249,13 +250,14 @@ let add_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
   let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
     let l = Univ.Universe.make l and r = Univ.Universe.make r in
-    let cstr' = match d with
+    let cstr' = let open UnivProblem in
+      match d with
       | Univ.Lt ->
-        Universes.ULe (Univ.Universe.super l, r)
-      | Univ.Le -> Universes.ULe (l, r)
-      | Univ.Eq -> Universes.UEq (l, r)
-    in Universes.Constraints.add cstr' acc)
-    cstrs Universes.Constraints.empty
+        ULe (Univ.Universe.super l, r)
+      | Univ.Le -> ULe (l, r)
+      | Univ.Eq -> UEq (l, r)
+    in UnivProblem.Set.add cstr' acc)
+    cstrs UnivProblem.Set.empty
   in
   let vars, weak, local' = process_universe_constraints ctx cstrs' in
   { ctx with
@@ -549,11 +551,11 @@ let is_sort_variable uctx s =
   | _ -> None
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst)
+  (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
 
 let normalize_variables uctx =
   let normalized_variables, undef, def, subst = 
-    Universes.normalize_univ_variables uctx.uctx_univ_variables 
+    UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
   let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
diff --git a/engine/uState.mli b/engine/uState.mli
index b1fcefb0a..11aaaf389 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -44,7 +44,7 @@ val context_set : t -> Univ.ContextSet.t
 (** The local context of the state, i.e. a set of bound variables together
     with their associated constraints. *)
 
-val subst : t -> Universes.universe_opt_subst
+val subst : t -> UnivSubst.universe_opt_subst
 (** The local universes that are unification variables *)
 
 val ugraph : t -> UGraph.t
@@ -79,7 +79,7 @@ val add_constraints : t -> Univ.Constraint.t -> t
   @raise UniversesDiffer when universes differ
 *)
 
-val add_universe_constraints : t -> Universes.Constraints.t -> t
+val add_universe_constraints : t -> UnivProblem.Set.t -> t
 (**
   @raise UniversesDiffer when universes differ
 *)
@@ -104,7 +104,7 @@ val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
 val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
-val merge_subst : t -> Universes.universe_opt_subst -> t
+val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
new file mode 100644
index 000000000..bc2edc13d
--- /dev/null
+++ b/engine/univProblem.ml
@@ -0,0 +1,166 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Univ
+open UnivSubst
+
+type t =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
+
+
+let is_trivial = function
+  | ULe (u, v) | UEq (u, v) -> Universe.equal u v
+  | ULub (u, v) | UWeak (u, v) -> Level.equal u v
+
+let subst_univs fn = function
+  | ULe (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | UEq (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | ULub (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (ULub (u',v'))
+  | UWeak (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (UWeak (u',v'))
+
+module Set = struct
+  module S = Set.Make(
+  struct
+    type nonrec t = t
+
+    let compare x y =
+      match x, y with
+      | ULe (u, v), ULe (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else i
+      | UEq (u, v), UEq (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else if Universe.equal u v' && Universe.equal v u' then 0
+        else i
+      | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
+        let i = Level.compare u u' in
+        if Int.equal i 0 then Level.compare v v'
+        else if Level.equal u v' && Level.equal v u' then 0
+        else i
+      | ULe _, _ -> -1
+      | _, ULe _ -> 1
+      | UEq _, _ -> -1
+      | _, UEq _ -> 1
+      | ULub _, _ -> -1
+      | _, ULub _ -> 1
+  end)
+
+  include S
+
+  let add cst s =
+    if is_trivial cst then s
+    else add cst s
+
+  let pr_one = let open Pp in function
+    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
+    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
+    | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
+    | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
+
+  let pr c =
+    let open Pp in
+    fold (fun cst pp_std ->
+        pp_std ++ pr_one cst ++ fnl ()) c (str "")
+
+  let equal x y =
+    x == y || equal x y
+
+  let subst_univs subst csts =
+    fold
+      (fun c -> Option.fold_right add (subst_univs subst c))
+      csts empty
+end
+
+type 'a accumulator = Set.t -> 'a -> 'a option
+type 'a constrained = 'a * Set.t
+
+type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t
+
+let enforce_eq_instances_univs strict x y c =
+  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
+  let ax = Instance.to_array x and ay = Instance.to_array y in
+    if Array.length ax != Array.length ay then
+      CErrors.anomaly Pp.(str "Invalid argument: enforce_eq_instances_univs called with" ++
+                          str " instances of different lengths.");
+    CArray.fold_right2
+      (fun x y -> Set.add (mk x y))
+      ax ay c
+
+let to_constraints ~force_weak g s =
+  let invalid () =
+    raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
+  in
+  let tr cst acc =
+    match cst with
+    | ULub (l, l') -> Constraint.add (l, Eq, l') acc
+    | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc
+    | UWeak  _-> acc
+    | ULe (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Le, l') acc
+        | None, Some _ -> enforce_leq l l' acc
+        | _, None ->
+          if UGraph.check_leq g l l'
+          then acc
+          else invalid ()
+      end
+    | UEq (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
+        | None, _ | _, None ->
+          if UGraph.check_eq g l l'
+          then acc
+          else invalid ()
+      end
+  in
+  Set.fold tr s Constraint.empty
+
+
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+    to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
+  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+     haven't find a way to factor the code without destroying
+     pointer-equality optimisations in [eq_constr_univs_infer].
+     Pointer equality is not sufficient to ensure equality up to
+     [kind1,kind2], because [kind1] and [kind2] may be different,
+     typically evaluating [m] and [n] in different evar maps. *)
+  let cstrs = ref accu in
+  let eq_universes _ _ = UGraph.check_eq_instances univs in
+  let eq_sorts s1 s2 =
+    if Sorts.equal s1 s2 then true
+    else
+      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+      match fold (Set.singleton (UEq (u1, u2))) !cstrs with
+      | None -> false
+      | Some accu -> cstrs := accu; true
+  in
+  let rec eq_constr' nargs m n =
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
+  in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
+  if res then Some !cstrs else None
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
new file mode 100644
index 000000000..ffaebe15a
--- /dev/null
+++ b/engine/univProblem.mli
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Univ
+
+(** {6 Constraints for type inference}
+
+    When doing conversion of universes, not only do we have =/<= constraints but
+    also Lub constraints which correspond to unification of two levels which might
+    not be necessary if unfolding is performed.
+
+    UWeak constraints come from irrelevant universes in cumulative polymorphism.
+*)
+
+type t =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
+
+val is_trivial : t -> bool
+
+module Set : sig
+  include Set.S with type elt = t
+
+  val pr : t -> Pp.t
+
+  val subst_univs : universe_subst_fn -> t -> t
+end
+
+type 'a accumulator = Set.t -> 'a -> 'a option
+type 'a constrained = 'a * Set.t
+type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t
+
+val enforce_eq_instances_univs : bool -> Instance.t constraint_function
+
+(** With [force_weak] UWeak constraints are turned into equalities,
+   otherwise they're forgotten. *)
+val to_constraints : force_weak:bool -> UGraph.t -> Set.t -> Constraint.t
+
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  UGraph.t -> 'a accumulator -> constr -> constr -> 'a -> 'a option
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
new file mode 100644
index 000000000..6a433d9fb
--- /dev/null
+++ b/engine/univSubst.ml
@@ -0,0 +1,177 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Sorts
+open Util
+open Pp
+open Constr
+open Univ
+
+let enforce_univ_constraint (u,d,v) =
+  match d with
+  | Eq -> enforce_eq u v
+  | Le -> enforce_leq u v
+  | Lt -> enforce_leq (super u) v
+
+let subst_univs_level fn l =
+  try Some (fn l)
+  with Not_found -> None
+
+let subst_univs_constraint fn (u,d,v as c) cstrs =
+  let u' = subst_univs_level fn u in
+  let v' = subst_univs_level fn v in
+  match u', v' with
+  | None, None -> Constraint.add c cstrs
+  | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
+  | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
+  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
+
+let subst_univs_constraints subst csts =
+  Constraint.fold
+    (fun c cstrs -> subst_univs_constraint subst c cstrs)
+    csts Constraint.empty
+
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_fn_constr f c =
+  let changed = ref false in
+  let fu = Univ.subst_univs_universe f in
+  let fi = Univ.Instance.subst_fn (level_subst_of f) in
+  let rec aux t =
+    match kind t with
+    | Sort (Sorts.Type u) ->
+      let u' = fu u in
+        if u' == u then t else
+          (changed := true; mkSort (Sorts.sort_of_univ u'))
+    | Const (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstU (c, u'))
+    | Ind (i, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkIndU (i, u'))
+    | Construct (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstructU (c, u'))
+    | _ -> map aux t
+  in
+  let c' = aux c in
+    if !changed then c' else c
+
+let subst_univs_constr subst c =
+  if Univ.is_empty_subst subst then c
+  else
+    let f = Univ.make_subst subst in
+      subst_univs_fn_constr f c
+
+let subst_univs_constr =
+  if Flags.profile then
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
+  else subst_univs_constr
+
+let normalize_univ_variable ~find =
+  let rec aux cur =
+    let b = find cur in
+    let b' = subst_univs_universe aux b in
+      if Universe.equal b' b then b
+      else b'
+  in aux
+
+let normalize_univ_variable_opt_subst ectx =
+  let find l =
+    match Univ.LMap.find l ectx with
+    | Some b -> b
+    | None -> raise Not_found
+  in
+  normalize_univ_variable ~find
+
+let normalize_univ_variable_subst subst =
+  let find l = Univ.LMap.find l subst in
+  normalize_univ_variable ~find
+
+let normalize_universe_opt_subst subst =
+  let normlevel = normalize_univ_variable_opt_subst subst in
+    subst_univs_universe normlevel
+
+let normalize_universe_subst subst =
+  let normlevel = normalize_univ_variable_subst subst in
+    subst_univs_universe normlevel
+
+let normalize_opt_subst ctx =
+  let normalize = normalize_universe_opt_subst ctx in
+  Univ.LMap.mapi (fun u -> function
+      | None -> None
+      | Some v -> Some (normalize v)) ctx
+
+type universe_opt_subst = Universe.t option universe_map
+
+let subst_univs_fn_puniverses f (c, u as cu) =
+  let u' = Instance.subst_fn f u in
+    if u' == u then cu else (c, u')
+
+let nf_evars_and_universes_opt_subst f subst =
+  let subst = normalize_univ_variable_opt_subst subst in
+  let lsubst = level_subst_of subst in
+  let rec aux c =
+    match kind c with
+    | Evar (evk, args) ->
+      let args = Array.map aux args in
+      (match try f (evk, args) with Not_found -> None with
+      | None -> mkEvar (evk, args)
+      | Some c -> aux c)
+    | Const pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_universe subst u in
+        if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> Constr.map aux c
+  in aux
+
+let make_opt_subst s =
+  fun x ->
+    (match Univ.LMap.find x s with
+    | Some u -> u
+    | None -> raise Not_found)
+
+let subst_opt_univs_constr s =
+  let f = make_opt_subst s in
+  subst_univs_fn_constr f
+
+let normalize_univ_variables ctx =
+  let ctx = normalize_opt_subst ctx in
+  let undef, def, subst =
+    Univ.LMap.fold (fun u v (undef, def, subst) ->
+      match v with
+      | None -> (Univ.LSet.add u undef, def, subst)
+      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
+    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
+  in ctx, undef, def, subst
+
+let pr_universe_body = function
+  | None -> mt ()
+  | Some v -> str" := " ++ Univ.Universe.pr v
+
+let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
diff --git a/engine/univSubst.mli b/engine/univSubst.mli
new file mode 100644
index 000000000..26e8d1db9
--- /dev/null
+++ b/engine/univSubst.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Univ
+
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+
+val subst_univs_constr : universe_subst -> constr -> constr
+
+type universe_opt_subst = Universe.t option universe_map
+
+val make_opt_subst : universe_opt_subst -> universe_subst_fn
+
+val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
+
+val normalize_univ_variables : universe_opt_subst ->
+  universe_opt_subst * LSet.t * LSet.t * universe_subst
+
+val normalize_univ_variable :
+  find:(Level.t -> Universe.t) ->
+  Level.t -> Universe.t
+
+val normalize_univ_variable_opt_subst : universe_opt_subst ->
+  (Level.t -> Universe.t)
+
+val normalize_univ_variable_subst : universe_subst ->
+  (Level.t -> Universe.t)
+
+val normalize_universe_opt_subst : universe_opt_subst ->
+  (Universe.t -> Universe.t)
+
+val normalize_universe_subst : universe_subst ->
+  (Universe.t -> Universe.t)
+
+val normalize_opt_subst : universe_opt_subst -> universe_opt_subst
+
+(** Full universes substitutions into terms *)
+
+val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
+  universe_opt_subst -> constr -> constr
+
+(** Pretty-printing *)
+
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
diff --git a/engine/universes.ml b/engine/universes.ml
index 01660fe04..009328571 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -8,11 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Sorts
 open Util
-open Pp
-open Constr
 open Univ
+open UnivSubst
 
 (* To disallow minimization to Set *)
 
@@ -27,190 +25,6 @@ let _ =
             optread  = is_set_minimization;
             optwrite = (:=) set_minimization })
 
-type universe_constraint =
-  | ULe of Universe.t * Universe.t
-  | UEq of Universe.t * Universe.t
-  | ULub of Level.t * Level.t
-  | UWeak of Level.t * Level.t
-
-module Constraints = struct
-  module S = Set.Make(
-  struct 
-    type t = universe_constraint
-
-    let compare x y =
-      match x, y with
-      | ULe (u, v), ULe (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
-        else i
-      | UEq (u, v), UEq (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
-        else if Universe.equal u v' && Universe.equal v u' then 0
-        else i
-      | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
-        let i = Level.compare u u' in
-        if Int.equal i 0 then Level.compare v v'
-        else if Level.equal u v' && Level.equal v u' then 0
-        else i
-      | ULe _, _ -> -1
-      | _, ULe _ -> 1
-      | UEq _, _ -> -1
-      | _, UEq _ -> 1
-      | ULub _, _ -> -1
-      | _, ULub _ -> 1
-  end)
-  
-  include S
-
-  let is_trivial = function
-    | ULe (u, v) | UEq (u, v) -> Universe.equal u v
-    | ULub (u, v) | UWeak (u, v) -> Level.equal u v
-
-  let add cst s =
-    if is_trivial cst then s
-    else add cst s
-
-  let pr_one = function
-    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
-    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
-    | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
-    | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
-
-  let pr c =
-    fold (fun cst pp_std ->
-        pp_std ++ pr_one cst ++ fnl ()) c (str "")
-
-  let equal x y = 
-    x == y || equal x y
-
-end
-
-type universe_constraints = Constraints.t
-type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
-type 'a universe_constrained = 'a * universe_constraints
-
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-let enforce_eq_instances_univs strict x y c = 
-  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
-  let ax = Instance.to_array x and ay = Instance.to_array y in
-    if Array.length ax != Array.length ay then
-      CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
-	       Pp.str " instances of different lengths.");
-    CArray.fold_right2
-      (fun x y -> Constraints.add (mk x y))
-      ax ay c
-
-let enforce_univ_constraint (u,d,v) =
-  match d with
-  | Eq -> enforce_eq u v
-  | Le -> enforce_leq u v
-  | Lt -> enforce_leq (super u) v
-
-let subst_univs_level fn l =
-  try Some (fn l)
-  with Not_found -> None
-
-let subst_univs_constraint fn (u,d,v as c) cstrs =
-  let u' = subst_univs_level fn u in
-  let v' = subst_univs_level fn v in
-  match u', v' with
-  | None, None -> Constraint.add c cstrs
-  | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs
-  | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs
-  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
-
-let subst_univs_constraints subst csts =
-  Constraint.fold
-    (fun c cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty
-
-let level_subst_of f =
-  fun l ->
-    try let u = f l in
-          match Universe.level u with
-          | None -> l
-          | Some l -> l
-    with Not_found -> l
-
-let subst_univs_universe_constraint fn = function
-  | ULe (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | UEq (u, v) ->
-    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (ULe (u',v'))
-  | ULub (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (ULub (u',v'))
-  | UWeak (u, v) ->
-    let u' = level_subst_of fn u and v' = level_subst_of fn v in
-    if Level.equal u' v' then None
-    else Some (UWeak (u',v'))
-
-let subst_univs_universe_constraints subst csts =
-  Constraints.fold 
-    (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c))
-    csts Constraints.empty 
-
-let to_constraints ~force_weak g s =
-  let invalid () =
-    raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
-  in
-  let tr cst acc =
-    match cst with
-    | ULub (l, l') -> Constraint.add (l, Eq, l') acc
-    | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc
-    | UWeak  _-> acc
-    | ULe (l, l') ->
-      begin match Universe.level l, Universe.level l' with
-        | Some l, Some l' -> Constraint.add (l, Le, l') acc
-        | None, Some _ -> enforce_leq l l' acc
-        | _, None ->
-          if UGraph.check_leq g l l'
-          then acc
-          else invalid ()
-      end
-    | UEq (l, l') ->
-      begin match Universe.level l, Universe.level l' with
-        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
-        | None, _ | _, None ->
-          if UGraph.check_eq g l l'
-          then acc
-          else invalid ()
-      end
-  in
-  Constraints.fold tr s Constraint.empty
-
-(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
-    to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
-  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
-     haven't find a way to factor the code without destroying
-     pointer-equality optimisations in [eq_constr_univs_infer].
-     Pointer equality is not sufficient to ensure equality up to
-     [kind1,kind2], because [kind1] and [kind2] may be different,
-     typically evaluating [m] and [n] in different evar maps. *)
-  let cstrs = ref accu in
-  let eq_universes _ _ = UGraph.check_eq_instances univs in
-  let eq_sorts s1 s2 = 
-    if Sorts.equal s1 s2 then true
-    else
-      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with
-      | None -> false
-      | Some accu -> cstrs := accu; true
-  in
-  let rec eq_constr' nargs m n =
-    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
-  in
-  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
-  if res then Some !cstrs else None
 
 (** Simplification *)
 
@@ -243,136 +57,6 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
-let subst_univs_fn_constr f c =
-  let changed = ref false in
-  let fu = Univ.subst_univs_universe f in
-  let fi = Univ.Instance.subst_fn (level_subst_of f) in
-  let rec aux t =
-    match kind t with
-    | Sort (Sorts.Type u) ->
-      let u' = fu u in
-        if u' == u then t else
-          (changed := true; mkSort (Sorts.sort_of_univ u'))
-    | Const (c, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkConstU (c, u'))
-    | Ind (i, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkIndU (i, u'))
-    | Construct (c, u) ->
-      let u' = fi u in
-        if u' == u then t
-        else (changed := true; mkConstructU (c, u'))
-    | _ -> map aux t
-  in
-  let c' = aux c in
-    if !changed then c' else c
-
-let subst_univs_constr subst c =
-  if Univ.is_empty_subst subst then c
-  else
-    let f = Univ.make_subst subst in
-      subst_univs_fn_constr f c
-
-let subst_univs_constr =
-  if Flags.profile then
-    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
-      CProfile.profile2 subst_univs_constr_key subst_univs_constr
-  else subst_univs_constr
-
-let normalize_univ_variable ~find =
-  let rec aux cur =
-    let b = find cur in
-    let b' = subst_univs_universe aux b in
-      if Universe.equal b' b then b
-      else b'
-  in aux
-
-let normalize_univ_variable_opt_subst ectx =
-  let find l = 
-    match Univ.LMap.find l ectx with
-    | Some b -> b
-    | None -> raise Not_found
-  in
-  normalize_univ_variable ~find
-
-let normalize_univ_variable_subst subst =
-  let find l = Univ.LMap.find l subst in
-  normalize_univ_variable ~find
-
-let normalize_universe_opt_subst subst =
-  let normlevel = normalize_univ_variable_opt_subst subst in
-    subst_univs_universe normlevel
-
-let normalize_universe_subst subst =
-  let normlevel = normalize_univ_variable_subst subst in
-    subst_univs_universe normlevel
-
-let normalize_opt_subst ctx = 
-  let normalize = normalize_universe_opt_subst ctx in
-  Univ.LMap.mapi (fun u -> function
-      | None -> None
-      | Some v -> Some (normalize v)) ctx
-
-type universe_opt_subst = Universe.t option universe_map
-
-let subst_univs_fn_puniverses f (c, u as cu) =
-  let u' = Instance.subst_fn f u in
-    if u' == u then cu else (c, u')
-
-let nf_evars_and_universes_opt_subst f subst =
-  let subst = normalize_univ_variable_opt_subst subst in
-  let lsubst = level_subst_of subst in
-  let rec aux c =
-    match kind c with
-    | Evar (evk, args) ->
-      let args = Array.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> mkEvar (evk, args)
-      | Some c -> aux c)
-    | Const pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkConstU pu'
-    | Ind pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkIndU pu'
-    | Construct pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-        if pu' == pu then c else mkConstructU pu'
-    | Sort (Type u) ->
-      let u' = Univ.subst_univs_universe subst u in
-        if u' == u then c else mkSort (sort_of_univ u')
-    | _ -> Constr.map aux c
-  in aux
-
-let make_opt_subst s = 
-  fun x -> 
-    (match Univ.LMap.find x s with
-    | Some u -> u
-    | None -> raise Not_found)
-
-let subst_opt_univs_constr s = 
-  let f = make_opt_subst s in
-  subst_univs_fn_constr f
-
-let normalize_univ_variables ctx = 
-  let ctx = normalize_opt_subst ctx in
-  let undef, def, subst =
-    Univ.LMap.fold (fun u v (undef, def, subst) -> 
-      match v with
-      | None -> (Univ.LSet.add u undef, def, subst)
-      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
-    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
-  in ctx, undef, def, subst
-
-let pr_universe_body = function
-  | None -> mt ()
-  | Some v -> str" := " ++ Univ.Universe.pr v
-
-let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
-
 (* Eq < Le < Lt *)
 let compare_constraint_type d d' =
   match d, d' with
@@ -448,6 +132,7 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts,
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
 let _pr_constraints_map (cmap:constraints_map) =
+  let open Pp in
   LMap.fold (fun l cstrs acc -> 
     Level.pr l ++ str " => " ++ 
       prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
@@ -763,3 +448,37 @@ let extend_context = UnivGen.extend_context
 let constr_of_global = UnivGen.constr_of_global
 let constr_of_reference = UnivGen.constr_of_global
 let type_of_global = UnivGen.type_of_global
+
+(** UnivSubst *)
+
+let level_subst_of = UnivSubst.level_subst_of
+let subst_univs_constraints = UnivSubst.subst_univs_constraints
+let subst_univs_constr = UnivSubst.subst_univs_constr
+type universe_opt_subst = UnivSubst.universe_opt_subst
+let make_opt_subst = UnivSubst.make_opt_subst
+let subst_opt_univs_constr = UnivSubst.subst_opt_univs_constr
+let normalize_univ_variables = UnivSubst.normalize_univ_variables
+let normalize_univ_variable = UnivSubst.normalize_univ_variable
+let normalize_univ_variable_opt_subst = UnivSubst.normalize_univ_variable_opt_subst
+let normalize_univ_variable_subst = UnivSubst.normalize_univ_variable_subst
+let normalize_universe_opt_subst = UnivSubst.normalize_universe_opt_subst
+let normalize_universe_subst = UnivSubst.normalize_universe_subst
+let nf_evars_and_universes_opt_subst = UnivSubst.nf_evars_and_universes_opt_subst
+let pr_universe_opt_subst = UnivSubst.pr_universe_opt_subst
+
+(** UnivProblem *)
+
+type universe_constraint = UnivProblem.t =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
+  | UWeak of Level.t * Level.t
+
+module Constraints = UnivProblem.Set
+type 'a constraint_accumulator = 'a UnivProblem.accumulator
+type 'a universe_constrained = 'a UnivProblem.constrained
+type 'a universe_constraint_function = 'a UnivProblem.constraint_function
+let subst_univs_universe_constraints = UnivProblem.Set.subst_univs
+let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs
+let to_constraints = UnivProblem.to_constraints
+let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with
diff --git a/engine/universes.mli b/engine/universes.mli
index bd315f277..3e397ed57 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -8,64 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Constr
 open Environ
 open Univ
+open UnivSubst
 
 (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
 module UPairSet : CSet.S with type elt = (Level.t * Level.t)
 
 (** Universes *)
 
-(** {6 Constraints for type inference}
-
-    When doing conversion of universes, not only do we have =/<= constraints but
-    also Lub constraints which correspond to unification of two levels which might
-    not be necessary if unfolding is performed.
-
-    UWeak constraints come from irrelevant universes in cumulative polymorphism.
-*)
-
-type universe_constraint =
-  | ULe of Universe.t * Universe.t
-  | UEq of Universe.t * Universe.t
-  | ULub of Level.t * Level.t
-  | UWeak of Level.t * Level.t
-
-module Constraints : sig
-  include Set.S with type elt = universe_constraint
-
-  val is_trivial : universe_constraint -> bool
-
-  val pr : t -> Pp.t
-end
-
-type universe_constraints = Constraints.t
-[@@ocaml.deprecated "Use Constraints.t"]
-
-type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option
-type 'a universe_constrained = 'a * Constraints.t
-type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t
-
-val subst_univs_universe_constraints : universe_subst_fn -> 
-  Constraints.t -> Constraints.t
-
-val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
-
-(** With [force_weak] UWeak constraints are turned into equalities,
-   otherwise they're forgotten. *)
-val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t
-
-(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
-    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
-    subterms of [m] and [n], arguments. *)
-val eq_constr_univs_infer_with :
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
-
 (** Simplification and pruning of constraints:
     [normalize_context_set ctx us]
 
@@ -77,53 +30,14 @@ val eq_constr_univs_infer_with :
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
-
-val subst_univs_constr : universe_subst -> constr -> constr
-
-type universe_opt_subst = Universe.t option universe_map
-
-val make_opt_subst : universe_opt_subst -> universe_subst_fn
-
-val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
-
 val normalize_context_set : UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
   (universe_opt_subst * LSet.t) in_universe_context_set
 
-val normalize_univ_variables : universe_opt_subst -> 
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
-
-val normalize_univ_variable : 
-  find:(Level.t -> Universe.t) ->
-  Level.t -> Universe.t
-
-val normalize_univ_variable_opt_subst : universe_opt_subst ->
-  (Level.t -> Universe.t)
-
-val normalize_univ_variable_subst : universe_subst ->
-  (Level.t -> Universe.t)
-
-val normalize_universe_opt_subst : universe_opt_subst ->
-  (Universe.t -> Universe.t)
-
-val normalize_universe_subst : universe_subst ->
-  (Universe.t -> Universe.t)
-
-(** Full universes substitutions into terms *)
-
-val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
-  universe_opt_subst -> constr -> constr
-
 val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
 
-(** Pretty-printing *)
-
-val pr_universe_opt_subst : universe_opt_subst -> Pp.t
-
 (** *********************************** Deprecated *)
 
 [@@@ocaml.warning "-3"]
@@ -246,3 +160,95 @@ val constr_of_reference : Globnames.global_reference -> constr
 
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 [@@ocaml.deprecated "Use [UnivGen.type_of_global]"]
+
+(** ****** Deprecated: moved to [UnivSubst] *)
+
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+[@@ocaml.deprecated "Use [UnivSubst.level_subst_of]"]
+
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constraints]"]
+
+val subst_univs_constr : universe_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constr]"]
+
+type universe_opt_subst = UnivSubst.universe_opt_subst
+[@@ocaml.deprecated "Use [UnivSubst.universe_opt_subst]"]
+
+val make_opt_subst : universe_opt_subst -> universe_subst_fn
+[@@ocaml.deprecated "Use [UnivSubst.make_opt_subst]"]
+
+val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"]
+
+val normalize_univ_variables : universe_opt_subst ->
+  universe_opt_subst * LSet.t * LSet.t * universe_subst
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"]
+
+val normalize_univ_variable :
+  find:(Level.t -> Universe.t) ->
+  Level.t -> Universe.t
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"]
+
+val normalize_univ_variable_opt_subst : universe_opt_subst ->
+  (Level.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_opt_subst]"]
+
+val normalize_univ_variable_subst : universe_subst ->
+  (Level.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_subst]"]
+
+val normalize_universe_opt_subst : universe_opt_subst ->
+  (Universe.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_opt_subst]"]
+
+val normalize_universe_subst : universe_subst ->
+  (Universe.t -> Universe.t)
+[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"]
+
+val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
+  universe_opt_subst -> constr -> constr
+[@@ocaml.deprecated "Use [UnivSubst.nf_evars_and_universes_opt_subst]"]
+
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
+[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"]
+
+(** ****** Deprecated: moved to [UnivProblem] *)
+
+type universe_constraint = UnivProblem.t =
+  | ULe of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.ULe]"]
+  | UEq of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.UEq]"]
+  | ULub of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.ULub]"]
+  | UWeak of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.UWeak]"]
+[@@ocaml.deprecated "Use [UnivProblem.t]"]
+
+module Constraints = UnivProblem.Set
+[@@ocaml.deprecated "Use [UnivProblem.Set]"]
+
+type 'a constraint_accumulator = 'a UnivProblem.accumulator
+[@@ocaml.deprecated "Use [UnivProblem.accumulator]"]
+type 'a universe_constrained = 'a UnivProblem.constrained
+[@@ocaml.deprecated "Use [UnivProblem.constrained]"]
+type 'a universe_constraint_function = 'a UnivProblem.constraint_function
+[@@ocaml.deprecated "Use [UnivProblem.constraint_function]"]
+
+val subst_univs_universe_constraints : universe_subst_fn ->
+  Constraints.t -> Constraints.t
+[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"]
+
+val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
+[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"]
+
+(** With [force_weak] UWeak constraints are turned into equalities,
+   otherwise they're forgotten. *)
+val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t
+[@@ocaml.deprecated "Use [UnivProblem.to_constraints]"]
+
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
+  UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
+[@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"]