Merge PR #7384: Split Universes

83 files changed, 1857 insertions, 1438 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8d5b5bef4..cb1abc4a9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -203,17 +203,17 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
-let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
 let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
-let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c23ba964c..63d7d5805 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : Univ.universe_subst -> unit
-val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
 val ppuniverse_level_subst : Univ.universe_level_subst -> unit
 val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
-val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
 val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
 val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
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 a5df5a9fa..37e83b623 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,3 +1,8 @@
+UnivNames
+UnivGen
+UnivSubst
+UnivProblem
+UnivMinim
 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 20a7c80ea..03b843655 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -804,19 +804,19 @@ let make_flexible_variable evd ~algebraic u =
 (****************************************)
 
 let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s)
 
 let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
 
 let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
 
 let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
@@ -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 509db525d..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,14 +543,14 @@ 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"]
 
 
 val evar_universe_context_of_binders :
-  Universes.universe_binders -> UState.t
+  UnivNames.universe_binders -> UState.t
 [@@ocaml.deprecated "Alias of UState.of_binders"]
 
 val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
@@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 
-val universe_binders : evar_map -> Universes.universe_binders
+val universe_binders : evar_map -> UnivNames.universe_binders
 val add_constraints_context : UState.t ->
   Univ.Constraint.t -> UState.t
 [@@ocaml.deprecated "Alias of UState.add_constraints"]
@@ -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 df43be28e..c271d9d99 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
 
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
@@ -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 df50bae86..844eb390b 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -20,14 +20,14 @@ type uinfo = {
   uloc : Loc.t option;
 }
 
-module UPairSet = Universes.UPairSet
+module UPairSet = UnivMinim.UPairSet
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { uctx_names : Universes.universe_binders * uinfo Univ.LMap.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
@@ -298,7 +300,7 @@ let reference_of_level uctx =
     fun l ->
       try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        Universes.reference_of_level l
+        UnivNames.reference_of_level l
 
 let pr_uctx_level uctx l =
   Libnames.pr_reference (reference_of_level uctx l)
@@ -471,7 +473,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level () in
+  let u = UnivGen.new_univ_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
@@ -549,14 +551,33 @@ 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 is_trivial_leq (l,d,r) =
+  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
+
+(* Prop < i <-> Set+1 <= i <-> Set < i *)
+let translate_cstr (l,d,r as cstr) =
+  let open Univ in
+  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
+    (Level.set, d, r)
+  else cstr
+
+let refresh_constraints univs (ctx, cstrs) =
+  let cstrs', univs' =
+    Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
+      let c = translate_cstr c in
+      if is_trivial_leq c then acc
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
+      cstrs (Univ.Constraint.empty, univs)
+  in ((ctx, cstrs'), univs')
 
 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
+  let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in
     subst, { uctx with uctx_local = ctx_local';
       uctx_univ_variables = normalized_variables;
       uctx_universes = univs }
@@ -582,7 +603,7 @@ let fix_undefined_variables uctx =
     uctx_univ_algebraic = algs' }
 
 let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
+  let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in
   let subst_fn u = Univ.subst_univs_level_level subst u in
   let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic Univ.LSet.empty 
@@ -609,7 +630,7 @@ let refresh_undefined_univ_variables uctx =
     uctx', subst
 
 let minimize uctx =
-  let open Universes in
+  let open UnivMinim in
   let ((vars',algs'), us') =
     normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
diff --git a/engine/uState.mli b/engine/uState.mli
index 48c38fafc..11aaaf389 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -34,9 +34,9 @@ val union : t -> t -> t
 
 val of_context_set : Univ.ContextSet.t -> t
 
-val of_binders : Universes.universe_binders -> t
+val of_binders : UnivNames.universe_binders -> t
 
-val universe_binders : t -> Universes.universe_binders
+val universe_binders : t -> UnivNames.universe_binders
 
 (** {5 Projections} *)
 
@@ -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/univGen.ml b/engine/univGen.ml
new file mode 100644
index 000000000..796a1bcc1
--- /dev/null
+++ b/engine/univGen.ml
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*         *   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 Names
+open Constr
+open Environ
+open Univ
+
+(* Generator of levels *)
+type universe_id = DirPath.t * int
+
+let new_univ_id, set_remote_new_univ_id =
+  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
+    ~build:(fun n -> Global.current_dirpath (), n)
+
+let new_univ_level () =
+  let dp, id = new_univ_id () in
+  Univ.Level.make dp id
+
+let fresh_level () = new_univ_level ()
+
+(* TODO: remove *)
+let new_univ dp = Univ.Universe.make (new_univ_level dp)
+let new_Type dp = mkType (new_univ dp)
+let new_Type_sort dp = Type (new_univ dp)
+
+let fresh_universe_instance ctx =
+  let init _ = new_univ_level () in
+  Instance.of_array (Array.init (AUContext.size ctx) init)
+
+let fresh_instance_from_context ctx =
+  let inst = fresh_universe_instance ctx in
+  let constraints = AUContext.instantiate inst ctx in
+    inst, constraints
+
+let fresh_instance ctx =
+  let ctx' = ref LSet.empty in
+  let init _ =
+    let u = new_univ_level () in
+    ctx' := LSet.add u !ctx'; u
+  in
+  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
+  in !ctx', inst
+
+let existing_instance ctx inst =
+  let () =
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx in
+      if not (len1 == len2) then
+        CErrors.user_err ~hdr:"Universes"
+          Pp.(str "Polymorphic constant expected " ++ int len2 ++
+              str" levels but was given " ++ int len1)
+      else ()
+  in LSet.empty, inst
+
+let fresh_instance_from ctx inst =
+  let ctx', inst =
+    match inst with
+    | Some inst -> existing_instance ctx inst
+    | None -> fresh_instance ctx
+  in
+  let constraints = AUContext.instantiate inst ctx in
+    inst, (ctx', constraints)
+
+(** Fresh universe polymorphic construction *)
+
+let fresh_constant_instance env c inst =
+  let cb = lookup_constant c env in
+  match cb.Declarations.const_universes with
+  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_const auctx ->
+    let inst, ctx =
+      fresh_instance_from auctx inst
+    in
+    ((c, inst), ctx)
+
+let fresh_inductive_instance env ind inst =
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    ((ind,Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind uactx ->
+    let inst, ctx = (fresh_instance_from uactx) inst in
+     ((ind,inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx =
+      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
+    in ((ind,inst), ctx)
+
+let fresh_constructor_instance env (ind,i) inst =
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  match mib.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
+  | Declarations.Polymorphic_ind auctx ->
+    let inst, ctx = fresh_instance_from auctx  inst in
+        (((ind,i),inst), ctx)
+  | Declarations.Cumulative_ind acumi ->
+    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
+    (((ind,i),inst), ctx)
+
+open Globnames
+
+let fresh_global_instance ?names env gr =
+  match gr with
+  | VarRef id -> mkVar id, ContextSet.empty
+  | ConstRef sp ->
+     let c, ctx = fresh_constant_instance env sp names in
+       mkConstU c, ctx
+  | ConstructRef sp ->
+     let c, ctx = fresh_constructor_instance env sp names in
+       mkConstructU c, ctx
+  | IndRef sp ->
+     let c, ctx = fresh_inductive_instance env sp names in
+       mkIndU c, ctx
+
+let fresh_constant_instance env sp =
+  fresh_constant_instance env sp None
+
+let fresh_inductive_instance env sp =
+  fresh_inductive_instance env sp None
+
+let fresh_constructor_instance env sp =
+  fresh_constructor_instance env sp None
+
+let constr_of_global gr =
+  let c, ctx = fresh_global_instance (Global.env ()) gr in
+    if not (Univ.ContextSet.is_empty ctx) then
+      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
+        (* Should be an error as we might forget constraints, allow for now
+           to make firstorder work with "using" clauses *)
+        c
+      else CErrors.user_err ~hdr:"constr_of_global"
+          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+              str " would forget universes.")
+    else c
+
+let constr_of_global_univ (gr,u) =
+  match gr with
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConstU (sp,u)
+  | ConstructRef sp -> mkConstructU (sp,u)
+  | IndRef sp -> mkIndU (sp,u)
+
+let fresh_global_or_constr_instance env = function
+  | IsConstr c -> c, ContextSet.empty
+  | IsGlobal gr -> fresh_global_instance env gr
+
+let global_of_constr c =
+  match kind c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Instance.empty
+  | _ -> raise Not_found
+
+open Declarations
+
+let type_of_reference env r =
+  match r with
+  | VarRef id -> Environ.named_type id env, ContextSet.empty
+  | ConstRef c ->
+     let cb = Environ.lookup_constant c env in
+     let ty = cb.const_type in
+     begin
+       match cb.const_universes with
+       | Monomorphic_const _ -> ty, ContextSet.empty
+       | Polymorphic_const auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+         Vars.subst_instance_constr inst ty, ctx
+     end
+  | IndRef ind ->
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+     begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
+         ty, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx  None in
+         let ty = Inductive.type_of_inductive env (specif, inst) in
+         ty, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx =
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
+         in
+         let ty = Inductive.type_of_inductive env (specif, inst) in
+         ty, ctx
+     end
+
+  | ConstructRef cstr ->
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    begin
+       match mib.mind_universes with
+       | Monomorphic_ind _ ->
+         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
+       | Polymorphic_ind auctx ->
+         let inst, ctx = fresh_instance_from auctx None in
+         Inductive.type_of_constructor (cstr,inst) specif, ctx
+       | Cumulative_ind cumi ->
+         let inst, ctx =
+           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
+         in
+         Inductive.type_of_constructor (cstr,inst) specif, ctx
+     end
+
+let type_of_global t = type_of_reference (Global.env ()) t
+
+let fresh_sort_in_family env = function
+  | InProp -> Sorts.prop, ContextSet.empty
+  | InSet -> Sorts.set, ContextSet.empty
+  | InType ->
+    let u = fresh_level () in
+      Type (Univ.Universe.make u), ContextSet.singleton u
+
+let new_sort_in_family sf =
+  fst (fresh_sort_in_family (Global.env ()) sf)
+
+let extend_context (a, ctx) (ctx') =
+  (a, ContextSet.union ctx ctx')
+
+let new_global_univ () =
+  let u = fresh_level () in
+  (Univ.Universe.make u, ContextSet.singleton u)
+
+let fresh_universe_context_set_instance ctx =
+  if ContextSet.is_empty ctx then LMap.empty, ctx
+  else
+    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
+    let univs',subst = LSet.fold
+      (fun u (univs',subst) ->
+        let u' = fresh_level () in
+          (LSet.add u' univs', LMap.add u u' subst))
+      univs (LSet.empty, LMap.empty)
+    in
+    let cst' = subst_univs_level_constraints subst cst in
+      subst, (univs', cst')
diff --git a/engine/univGen.mli b/engine/univGen.mli
new file mode 100644
index 000000000..8169dbda4
--- /dev/null
+++ b/engine/univGen.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*         *   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 Names
+open Constr
+open Environ
+open Univ
+
+
+(** The global universe counter *)
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+
+(** Side-effecting functions creating new universe levels. *)
+
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
+
+val new_global_univ : unit -> Universe.t in_universe_context_set
+val new_sort_in_family : Sorts.family -> Sorts.t
+
+(** Build a fresh instance for a given context, its associated substitution and
+    the instantiated constraints. *)
+
+val fresh_instance_from_context : AUContext.t ->
+  Instance.t constrained
+
+val fresh_instance_from : AUContext.t -> Instance.t option ->
+  Instance.t in_universe_context_set
+
+val fresh_sort_in_family : env -> Sorts.family ->
+  Sorts.t in_universe_context_set
+val fresh_constant_instance : env -> Constant.t ->
+  pconstant in_universe_context_set
+val fresh_inductive_instance : env -> inductive ->
+  pinductive in_universe_context_set
+val fresh_constructor_instance : env -> constructor ->
+  pconstructor in_universe_context_set
+
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+  constr in_universe_context_set
+
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
+  constr in_universe_context_set
+
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : ContextSet.t ->
+  universe_level_subst * ContextSet.t
+
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> GlobRef.t puniverses
+
+val constr_of_global_univ : GlobRef.t puniverses -> constr
+
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+
+(** Create a fresh global in the global environment, without side effects.
+    BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+    the constraints should be properly added to an evd.
+    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
+    the proper way to get a fresh copy of a global reference. *)
+val constr_of_global : GlobRef.t -> constr
+
+(** Returns the type of the global reference, by creating a fresh instance of polymorphic
+    references and computing their instantiated universe context. (side-effect on the
+    universe counter, use with care). *)
+val type_of_global : GlobRef.t -> types in_universe_context_set
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
new file mode 100644
index 000000000..f10e6d2ec
--- /dev/null
+++ b/engine/univMinim.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(*         *   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
+
+(* To disallow minimization to Set *)
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+
+let _ =
+  Goptions.(declare_bool_option
+          { optdepr  = false;
+            optname  = "minimization to Set";
+            optkey   = ["Universe";"Minimization";"ToSet"];
+            optread  = is_set_minimization;
+            optwrite = (:=) set_minimization })
+
+
+(** Simplification *)
+
+let add_list_map u t map =
+  try
+    let l = LMap.find u map in
+    LMap.set u (t :: l) map
+  with Not_found ->
+    LMap.add u [t] map
+
+(** Precondition: flexible <= ctx *)
+let choose_canonical ctx flexible algs s =
+  let global = LSet.diff s ctx in
+  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
+    (** If there is a global universe in the set, choose it *)
+    if not (LSet.is_empty global) then
+      let canon = LSet.choose global in
+        canon, (LSet.remove canon global, rigid, flexible)
+    else (** No global in the equivalence class, choose a rigid one *)
+        if not (LSet.is_empty rigid) then
+          let canon = LSet.choose rigid in
+            canon, (global, LSet.remove canon rigid, flexible)
+        else (** There are only flexible universes in the equivalence
+                 class, choose a non-algebraic. *)
+          let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
+            if not (LSet.is_empty nonalgs) then
+              let canon = LSet.choose nonalgs in
+                canon, (global, rigid, LSet.remove canon flexible)
+            else
+              let canon = LSet.choose algs in
+                canon, (global, rigid, LSet.remove canon flexible)
+
+(* Eq < Le < Lt *)
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq -> 0
+  | Eq, _ -> -1
+  | _, Eq -> 1
+  | Le, Le -> 0
+  | Le, _ -> -1
+  | _, Le -> 1
+  | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+  let merge k a b =
+    match a, b with
+    | Some _, None -> a
+    | None, Some _ -> b
+    | None, None -> None
+    | Some l, Some r ->
+       if compare_constraint_type l r >= 0 then a
+       else b
+  in LMap.merge merge
+
+let lower_add l c m =
+  try let c' = LMap.find l m in
+      if compare_constraint_type c c' > 0 then
+        LMap.add l c m
+      else m
+  with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
+
+exception Found of Level.t * lowermap
+let find_inst insts v =
+  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
+    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
+        insts; raise Not_found
+  with Found (f,l) -> (f,l)
+
+let compute_lbound left =
+ (** The universe variable was not fixed yet.
+     Compute its level using its lower bound. *)
+  let sup l lbound =
+    match lbound with
+    | None -> Some l
+    | Some l' -> Some (Universe.sup l l')
+  in
+    List.fold_left (fun lbound (d, l) ->
+      if d == Le (* l <= ?u *) then sup l lbound
+      else (* l < ?u *)
+        (assert (d == Lt);
+         if not (Universe.level l == None) then
+           sup (Universe.super l) lbound
+         else None))
+      None left
+
+let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
+  if enforce then
+    let inst = Universe.make u in
+    let cstrs' = enforce_leq lbound inst cstrs in
+      (ctx, us, LSet.remove u algs,
+       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
+      {enforce; alg; lbound=inst; lower}
+  else (* Actually instantiate *)
+    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
+     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
+    {enforce; alg; lbound; lower}
+
+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 ++
+      fnl () ++ acc)
+    cmap (mt ())
+
+let remove_alg l (ctx, us, algs, insts, cstrs) =
+  (ctx, us, LSet.remove l algs, insts, cstrs)
+
+let not_lower lower (d,l) =
+  (* We're checking if (d,l) is already implied by the lower
+     constraints on some level u. If it represents l < u (d is Lt
+     or d is Le and i > 0, the i < 0 case is impossible due to
+     invariants of Univ), and the lower constraints only have l <=
+     u then it is not implied. *)
+  Univ.Universe.exists
+    (fun (l,i) ->
+       let d =
+         if i == 0 then d
+         else match d with
+           | Le -> Lt
+           | d -> d
+       in
+       try let d' = LMap.find l lower in
+         (* If d is stronger than the already implied lower
+          * constraints we must keep it. *)
+         compare_constraint_type d d' > 0
+       with Not_found ->
+         (** No constraint existing on l *) true) l
+
+exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+   constraints to [lbound], adding them to [cstrs].
+
+    @raise UpperBoundedAlg if any [upper] constraints are strict and
+   [lbound] algebraic. *)
+let enforce_uppers upper lbound cstrs =
+  List.fold_left (fun cstrs (d, r) ->
+      if d == Univ.Le then
+        enforce_leq lbound (Universe.make r) cstrs
+      else
+        match Universe.level lbound with
+        | Some lev -> Constraint.add (lev, d, r) cstrs
+        | None -> raise UpperBoundedAlg)
+    cstrs upper
+
+let minimize_univ_variables ctx us algs left right cstrs =
+  let left, lbounds =
+    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
+      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
+      else (* Fixed universe, just compute its glb for sharing *)
+        let lbounds =
+          match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
+          | None -> lbounds
+          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
+                                   lbounds
+        in (Univ.LMap.remove r left, lbounds))
+      left (left, Univ.LMap.empty)
+  in
+  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
+    let acc, left, lower =
+      match LMap.find u left with
+      | exception Not_found -> acc, [], LMap.empty
+      | l ->
+        let acc, left, newlow, lower =
+          List.fold_left
+          (fun (acc, left, newlow, lower') (d, l) ->
+           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
+           let l' =
+             if enf then Universe.make l
+             else l'
+           in acc', (d, l') :: left,
+              lower_add l d newlow, lower_union lower lower')
+          (acc, [], LMap.empty, LMap.empty) l
+        in
+        let left = CList.uniquize (List.filter (not_lower lower) left) in
+        (acc, left, LMap.union newlow lower)
+    in
+    let instantiate_lbound lbound =
+      let alg = LSet.mem u algs in
+        if alg then
+          (* u is algebraic: we instantiate it with its lower bound, if any,
+              or enforce the constraints if it is bounded from the top. *)
+          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
+          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
+        else (* u is non algebraic *)
+          match Universe.level lbound with
+          | Some l -> (* The lowerbound is directly a level *)
+             (* u is not algebraic but has no upper bounds,
+                we instantiate it with its lower bound if it is a
+                different level, otherwise we keep it. *)
+             let lower = LMap.remove l lower in
+             if not (Level.equal l u) then
+               (* Should check that u does not
+                  have upper constraints that are not already in right *)
+               let acc = remove_alg l acc in
+                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
+             else acc, {enforce=true; alg=false; lbound; lower}
+          | None ->
+            begin match find_inst insts lbound with
+              | can, lower ->
+                (* Another universe represents the same lower bound,
+                   we can share them with no harm. *)
+                let lower = LMap.remove can lower in
+                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
+              | exception Not_found ->
+                (* We set u as the canonical universe representing lbound *)
+                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
+            end
+    in
+    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
+      match LMap.find u right with
+      | exception Not_found -> acc
+      | upper ->
+        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
+        let cstrs = enforce_uppers upper b.lbound cstrs in
+        (ctx, us, algs, insts, cstrs), b
+    in
+    if not (LSet.mem u ctx)
+    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+    else
+      let lbound = compute_lbound left in
+      match lbound with
+      | None -> (* Nothing to do *)
+        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
+      | Some lbound ->
+        try enforce_uppers (instantiate_lbound lbound)
+        with UpperBoundedAlg ->
+          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
+  and aux (ctx, us, algs, seen, cstrs as acc) u =
+    try acc, LMap.find u seen
+    with Not_found -> instance acc u
+  in
+    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
+      if v == None then fst (aux acc u)
+      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
+      us (ctx, us, algs, lbounds, cstrs)
+
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
+let normalize_context_set g ctx us algs weak =
+  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
+  (** Keep the Prop/Set <= i constraints separate for minimization *)
+  let smallles, csts =
+    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+  in
+  let smallles = if is_set_minimization ()
+    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+    else Constraint.empty
+  in
+  let csts, partition =
+    (* We first put constraints in a normal-form: all self-loops are collapsed
+       to equalities. *)
+    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+                           ctx UGraph.initial_universes
+    in
+    let add_soft u g =
+      if not (Level.is_small u || LSet.mem u ctx)
+      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      else g
+    in
+    let g = Constraint.fold
+        (fun (l, d, r) g -> add_soft r (add_soft l g))
+        csts g
+    in
+    let g = UGraph.merge_constraints csts g in
+      UGraph.constraints_of_universes g
+  in
+  (* We ignore the trivial Prop/Set <= i constraints. *)
+  let noneqs =
+    Constraint.filter
+      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+                           (Level.is_prop l && d == Lt && Level.is_set r)))
+      csts
+  in
+  let noneqs = Constraint.union noneqs smallles in
+  let flex x = LMap.mem x us in
+  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
+    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
+    (* Add equalities for globals which can't be merged anymore. *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) global
+      cstrs
+    in
+    (* Also add equalities for rigid variables *)
+    let cstrs = LSet.fold (fun g cst ->
+      Constraint.add (canon, Eq, g) cst) rigid
+      cstrs
+    in
+    let canonu = Some (Universe.make canon) in
+    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
+      (LSet.diff ctx flexible, us, cstrs))
+    (ctx, us, Constraint.empty) partition
+  in
+  (* Process weak constraints: when one side is flexible and the 2
+     universes are unrelated unify them. *)
+  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
+      let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+      let u = norm u and v = norm v in
+      let set_to a b =
+        (LSet.remove a ctx,
+         LMap.add a (Some (Universe.make b)) us,
+         UGraph.enforce_constraint (a,Eq,b) g)
+      in
+      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
+      then acc
+      else
+      if LMap.mem u us
+      then set_to u v
+      else if LMap.mem v us
+      then set_to v u
+      else acc)
+      weak (ctx, us, g)  in
+  (* Noneqs is now in canonical form w.r.t. equality constraints,
+     and contains only inequality constraints. *)
+  let noneqs =
+    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
+    Constraint.fold (fun (u,d,v) noneqs ->
+        let u = norm u and v = norm v in
+        if d != Lt && Level.equal u v then noneqs
+        else Constraint.add (u,d,v) noneqs)
+      noneqs Constraint.empty
+  in
+  (* Compute the left and right set of flexible variables, constraints
+     mentionning other variables remain in noneqs. *)
+  let noneqs, ucstrsl, ucstrsr =
+    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
+      let lus = LMap.mem l us and rus = LMap.mem r us in
+      let ucstrsl' =
+        if lus then add_list_map l (d, r) ucstrsl
+        else ucstrsl
+      and ucstrsr' =
+        add_list_map r (d, l) ucstrsr
+      in
+      let noneqs =
+        if lus || rus then noneq
+        else Constraint.add cstr noneq
+      in (noneqs, ucstrsl', ucstrsr'))
+    noneqs (Constraint.empty, LMap.empty, LMap.empty)
+  in
+  (* Now we construct the instantiation of each variable. *)
+  let ctx', us, algs, inst, noneqs =
+    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
+  in
+  let us = normalize_opt_subst us in
+    (us, algs), (ctx', Constraint.union noneqs eqs)
+
+(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
new file mode 100644
index 000000000..9f80b7acb
--- /dev/null
+++ b/engine/univMinim.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   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
+
+(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
+module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+
+(** Simplification and pruning of constraints:
+    [normalize_context_set ctx us]
+
+    - Instantiate the variables in [us] with their most precise
+    universe levels respecting the constraints.
+
+    - Normalizes the context [ctx] w.r.t. equality constraints,
+    choosing a canonical universe in each equivalence class
+    (a global one if there is one) and transitively saturate
+    the constraints w.r.t to the equalities. *)
+
+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
diff --git a/engine/univNames.ml b/engine/univNames.ml
new file mode 100644
index 000000000..6e59a7c9e
--- /dev/null
+++ b/engine/univNames.ml
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*         *   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 Names
+open Univ
+open Globnames
+open Nametab
+
+
+let reference_of_level l = CAst.make @@
+  match Level.name l with
+  | Some (d, n as na)  ->
+     let qid =
+       try Nametab.shortest_qualid_of_universe na
+       with Not_found ->
+         let name = Id.of_string_soft (string_of_int n) in
+         Libnames.make_qualid d name
+     in Libnames.Qualid qid
+  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
+
+let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+  match Level.name u with
+  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+  | None -> ()
+
+let is_polymorphic l =
+  match Level.name l with
+  | Some n ->
+     (try Nametab.UnivIdMap.find n !universe_map
+      with Not_found -> false)
+  | None -> false
+
+(** Local universe names of polymorphic references *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref : universe_binders =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> Names.Id.Map.empty
+
+let cache_ubinder (_,(ref,l)) =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+
+let subst_ubinder (subst,(ref,l as orig)) =
+  let ref' = fst (Globnames.subst_global subst ref) in
+  if ref == ref' then orig else ref', l
+
+let discharge_ubinder (_,(ref,l)) =
+  Some (Lib.discharge_global ref, l)
+
+let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+  let open Libobject in
+  declare_object { (default_object "universe binder") with
+    cache_function = cache_ubinder;
+    load_function = (fun _ x -> cache_ubinder x);
+    classify_function = (fun x -> Substitute x);
+    subst_function = subst_ubinder;
+    discharge_function = discharge_ubinder;
+    rebuild_function = (fun x -> x); }
+
+let register_universe_binders ref ubinders =
+  (* Add the polymorphic (section) universes *)
+  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+    let qid = Nametab.shortest_qualid_of_universe lvl in
+    let level = Level.make (fst lvl) (snd lvl) in
+    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+    else ubinders)
+    !universe_map ubinders
+  in
+  if not (Id.Map.is_empty ubinders)
+  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+
+type univ_name_list = Misctypes.lname list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
diff --git a/engine/univNames.mli b/engine/univNames.mli
new file mode 100644
index 000000000..e3bc3193d
--- /dev/null
+++ b/engine/univNames.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*         *   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
+
+val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+    polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+(** Is [lvl]  a global polymorphic universe? (ie section polymorphic universe) *)
+val is_polymorphic : Level.t -> bool
+
+(** Local universe name <-> level mapping *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
+
+val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val universe_binders_of_global : Names.GlobRef.t -> universe_binders
+
+type univ_name_list = Misctypes.lname list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Names.GlobRef.t ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
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 a13663cba..70601987c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -8,1098 +8,90 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Sorts
-open Util
-open Pp
-open Names
-open Constr
-open Environ
 open Univ
-open Globnames
-open Nametab
 
-module UPairs = OrderedType.UnorderedPair(Univ.Level)
-module UPairSet = Set.Make (UPairs)
-
-let reference_of_level l = CAst.make @@
-  match Level.name l with
-  | Some (d, n as na)  ->
-     let qid =
-       try Nametab.shortest_qualid_of_universe na
-       with Not_found ->
-         let name = Id.of_string_soft (string_of_int n) in
-         Libnames.make_qualid d name
-     in Libnames.Qualid qid
-  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
-
-(** Global universe information outside the kernel, to handle
-    polymorphic universe names in sections that have to be discharged. *)
-
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
-  match Level.name u with
-  | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
-  | None -> ()
-
-let is_polymorphic l =
-  match Level.name l with
-  | Some n ->
-     (try Nametab.UnivIdMap.find n !universe_map
-      with Not_found -> false)
-  | None -> false
-
-(** Local universe names of polymorphic references *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-let empty_binders = Id.Map.empty
-
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : universe_binders =
-  try
-    let l = Refmap.find ref !universe_binders_table in l
-  with Not_found -> Names.Id.Map.empty
-
-let cache_ubinder (_,(ref,l)) =
-  universe_binders_table := Refmap.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
-  let ref' = fst (Globnames.subst_global subst ref) in
-  if ref == ref' then orig else ref', l
-
-let discharge_ubinder (_,(ref,l)) =
-  Some (Lib.discharge_global ref, l)
-
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
-  let open Libobject in
-  declare_object { (default_object "universe binder") with
-    cache_function = cache_ubinder;
-    load_function = (fun _ x -> cache_ubinder x);
-    classify_function = (fun x -> Substitute x);
-    subst_function = subst_ubinder;
-    discharge_function = discharge_ubinder;
-    rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref ubinders =
-  let open Names in
-  (* Add the polymorphic (section) universes *)
-  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
-    let qid = Nametab.shortest_qualid_of_universe lvl in
-    let level = Level.make (fst lvl) (snd lvl) in
-    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
-    else ubinders)
-    !universe_map ubinders
-  in
-  if not (Id.Map.is_empty ubinders)
-  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-
-type univ_name_list = Misctypes.lname list
-
-let universe_binders_with_opt_names ref levels = function
-  | None -> universe_binders_of_global ref
-  | Some udecl ->
-    if Int.equal(List.length levels) (List.length udecl)
-    then
-      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
-          | Anonymous -> acc
-          | Name na -> Names.Id.Map.add na lvl acc)
-        empty_binders udecl levels
-    else
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
-
-(* To disallow minimization to Set *)
-
-let set_minimization = ref true
-let is_set_minimization () = !set_minimization
-			    
-type universe_constraint =
+(** Deprecated *)
+
+(** UnivNames *)
+type universe_binders = UnivNames.universe_binders
+type univ_name_list = UnivNames.univ_name_list
+
+let pr_with_global_universes = UnivNames.pr_with_global_universes
+let reference_of_level = UnivNames.reference_of_level
+
+let add_global_universe = UnivNames.add_global_universe
+
+let is_polymorphic = UnivNames.is_polymorphic
+
+let empty_binders = UnivNames.empty_binders
+
+let register_universe_binders = UnivNames.register_universe_binders
+let universe_binders_of_global = UnivNames.universe_binders_of_global
+
+let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
+
+(** UnivGen *)
+type universe_id = UnivGen.universe_id
+
+let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id
+let new_univ_id = UnivGen.new_univ_id
+let new_univ_level = UnivGen.new_univ_level
+let new_univ = UnivGen.new_univ
+let new_Type = UnivGen.new_Type
+let new_Type_sort = UnivGen.new_Type_sort
+let new_global_univ = UnivGen.new_global_univ
+let new_sort_in_family = UnivGen.new_sort_in_family
+let fresh_instance_from_context = UnivGen.fresh_instance_from_context
+let fresh_instance_from = UnivGen.fresh_instance_from
+let fresh_sort_in_family = UnivGen.fresh_sort_in_family
+let fresh_constant_instance = UnivGen.fresh_constant_instance
+let fresh_inductive_instance = UnivGen.fresh_inductive_instance
+let fresh_constructor_instance = UnivGen.fresh_constructor_instance
+let fresh_global_instance = UnivGen.fresh_global_instance
+let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance
+let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance
+let global_of_constr = UnivGen.global_of_constr
+let constr_of_global_univ = UnivGen.constr_of_global_univ
+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 = 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
-
-(* Generator of levels *)
-type universe_id = DirPath.t * int
-
-let new_univ_id, set_remote_new_univ_id =
-  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Global.current_dirpath (), n)
-
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
-
-let fresh_level () = new_univ_level ()
-
-(* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
-
-let fresh_universe_instance ctx =
-  let init _ = new_univ_level () in
-  Instance.of_array (Array.init (AUContext.size ctx) init)
-
-let fresh_instance_from_context ctx =
-  let inst = fresh_universe_instance ctx in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, constraints
-
-let fresh_instance ctx =
-  let ctx' = ref LSet.empty in
-  let init _ =
-    let u = new_univ_level () in
-    ctx' := LSet.add u !ctx'; u
-  in
-  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
-  in !ctx', inst
-
-let existing_instance ctx inst = 
-  let () = 
-    let len1 = Array.length (Instance.to_array inst)
-    and len2 = AUContext.size ctx in
-      if not (len1 == len2) then
-	CErrors.user_err ~hdr:"Universes"
-	  (str "Polymorphic constant expected " ++ int len2 ++ 
-	     str" levels but was given " ++ int len1)
-      else ()
-  in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
-  let ctx', inst = 
-    match inst with 
-    | Some inst -> existing_instance ctx inst
-    | None -> fresh_instance ctx 
-  in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, (ctx', constraints)
-
-(** Fresh universe polymorphic construction *)
-
-let fresh_constant_instance env c inst =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_const auctx -> 
-    let inst, ctx =
-      fresh_instance_from auctx inst
-    in
-    ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    ((ind,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind uactx ->
-    let inst, ctx = (fresh_instance_from uactx) inst in 
-     ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = 
-      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
-    in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = fresh_instance_from auctx  inst in
-	(((ind,i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
-    (((ind,i),inst), ctx)
-
-open Globnames
-
-let fresh_global_instance ?names env gr =
-  match gr with
-  | VarRef id -> mkVar id, ContextSet.empty
-  | ConstRef sp -> 
-     let c, ctx = fresh_constant_instance env sp names in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = fresh_constructor_instance env sp names in
-       mkConstructU c, ctx
-  | IndRef sp -> 
-     let c, ctx = fresh_inductive_instance env sp names in
-       mkIndU c, ctx
-
-let fresh_constant_instance env sp = 
-  fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp = 
-  fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp = 
-  fresh_constructor_instance env sp None
-
-let constr_of_global gr =
-  let c, ctx = fresh_global_instance (Global.env ()) gr in
-    if not (Univ.ContextSet.is_empty ctx) then
-      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then 
-	(* Should be an error as we might forget constraints, allow for now
-	   to make firstorder work with "using" clauses *)
-	c
-      else CErrors.user_err ~hdr:"constr_of_global"
-          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
-	      str " would forget universes.")
-    else c
-
-let constr_of_reference = constr_of_global
-
-let constr_of_global_univ (gr,u) =
-  match gr with
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConstU (sp,u)
-  | ConstructRef sp -> mkConstructU (sp,u)
-  | IndRef sp -> mkIndU (sp,u)
-
-let fresh_global_or_constr_instance env = function
-  | IsConstr c -> c, ContextSet.empty
-  | IsGlobal gr -> fresh_global_instance env gr
-
-let global_of_constr c =
-  match kind c with
-  | Const (c, u) -> ConstRef c, u
-  | Ind (i, u) -> IndRef i, u
-  | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Instance.empty
-  | _ -> raise Not_found
-
-open Declarations
-
-let type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env, ContextSet.empty
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-     let ty = cb.const_type in
-     begin
-       match cb.const_universes with
-       | Monomorphic_const _ -> ty, ContextSet.empty
-       | Polymorphic_const auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Vars.subst_instance_constr inst ty, ctx
-     end
-  | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
-	 ty, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx  None in
-	 let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx = 
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-     end
-	 
-  | ConstructRef cstr ->
-    let (mib,oib as specif) = 
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
-    in
-    begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-	 Inductive.type_of_constructor (cstr,inst) specif, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx = 
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None 
-         in
-	 Inductive.type_of_constructor (cstr,inst) specif, ctx
-     end
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
-let fresh_sort_in_family env = function
-  | InProp -> Sorts.prop, ContextSet.empty
-  | InSet -> Sorts.set, ContextSet.empty
-  | InType -> 
-    let u = fresh_level () in
-      Type (Univ.Universe.make u), ContextSet.singleton u
-
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family (Global.env ()) sf)
-
-let extend_context (a, ctx) (ctx') =
-  (a, ContextSet.union ctx ctx')
-
-let new_global_univ () =
-  let u = fresh_level () in
-    (Univ.Universe.make u, ContextSet.singleton u)
-
-(** Simplification *)
-
-let add_list_map u t map =
-  try
-    let l = LMap.find u map in
-    LMap.set u (t :: l) map
-  with Not_found ->
-    LMap.add u [t] map
-
-(** Precondition: flexible <= ctx *)
-let choose_canonical ctx flexible algs s =
-  let global = LSet.diff s ctx in
-  let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
-    (** If there is a global universe in the set, choose it *)
-    if not (LSet.is_empty global) then
-      let canon = LSet.choose global in
-	canon, (LSet.remove canon global, rigid, flexible)
-    else (** No global in the equivalence class, choose a rigid one *)
-	if not (LSet.is_empty rigid) then
-	  let canon = LSet.choose rigid in
-	    canon, (global, LSet.remove canon rigid, flexible)
-	else (** There are only flexible universes in the equivalence
-		 class, choose a non-algebraic. *)
-	  let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
-	    if not (LSet.is_empty nonalgs) then
-	      let canon = LSet.choose nonalgs in
-		canon, (global, rigid, LSet.remove canon flexible)
-	    else
-	      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 fresh_universe_context_set_instance ctx =
-  if ContextSet.is_empty ctx then LMap.empty, ctx
-  else
-    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
-    let univs',subst = LSet.fold
-      (fun u (univs',subst) ->
-	let u' = fresh_level () in
-	  (LSet.add u' univs', LMap.add u u' subst))
-      univs (LSet.empty, LMap.empty)
-    in
-    let cst' = subst_univs_level_constraints subst cst in
-      subst, (univs', cst')
-
-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
-  | Eq, Eq -> 0
-  | Eq, _ -> -1
-  | _, Eq -> 1
-  | Le, Le -> 0
-  | Le, _ -> -1
-  | _, Le -> 1
-  | Lt, Lt -> 0
-
-type lowermap = constraint_type LMap.t
-
-let lower_union =
-  let merge k a b =
-    match a, b with
-    | Some _, None -> a
-    | None, Some _ -> b
-    | None, None -> None
-    | Some l, Some r ->
-       if compare_constraint_type l r >= 0 then a
-       else b
-  in LMap.merge merge
-
-let lower_add l c m =
-  try let c' = LMap.find l m in
-      if compare_constraint_type c c' > 0 then
-        LMap.add l c m
-      else m
-  with Not_found -> LMap.add l c m
-
-let lower_of_list l =
-  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
-
-type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap }
-
-exception Found of Level.t * lowermap
-let find_inst insts v =
-  try LMap.iter (fun k {enforce;alg;lbound=v';lower} ->
-    if not alg && enforce && Universe.equal v' v then raise (Found (k, lower)))
-	insts; raise Not_found
-  with Found (f,l) -> (f,l)
-
-let compute_lbound left =
- (** The universe variable was not fixed yet.
-     Compute its level using its lower bound. *)
-  let sup l lbound = 
-    match lbound with
-    | None -> Some l
-    | Some l' -> Some (Universe.sup l l')
-  in
-    List.fold_left (fun lbound (d, l) -> 
-      if d == Le (* l <= ?u *) then sup l lbound
-      else (* l < ?u *) 
-	(assert (d == Lt); 
-	 if not (Universe.level l == None) then
-	   sup (Universe.super l) lbound
-	 else None))
-      None left
-
-let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) =
-  if enforce then
-    let inst = Universe.make u in
-    let cstrs' = enforce_leq lbound inst cstrs in
-      (ctx, us, LSet.remove u algs, 
-       LMap.add u {enforce;alg;lbound;lower} insts, cstrs'),
-      {enforce; alg; lbound=inst; lower}
-  else (* Actually instantiate *)
-    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u {enforce;alg;lbound;lower} insts, cstrs),
-    {enforce; alg; lbound; lower}
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-let _pr_constraints_map (cmap:constraints_map) =
-  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 ++
-      fnl () ++ acc)
-    cmap (mt ())
-
-let remove_alg l (ctx, us, algs, insts, cstrs) =
-  (ctx, us, LSet.remove l algs, insts, cstrs)
-
-let not_lower lower (d,l) =
-  (* We're checking if (d,l) is already implied by the lower
-     constraints on some level u. If it represents l < u (d is Lt
-     or d is Le and i > 0, the i < 0 case is impossible due to
-     invariants of Univ), and the lower constraints only have l <=
-     u then it is not implied. *)
-  Univ.Universe.exists
-    (fun (l,i) ->
-       let d =
-         if i == 0 then d
-         else match d with
-           | Le -> Lt
-           | d -> d
-       in
-       try let d' = LMap.find l lower in
-         (* If d is stronger than the already implied lower
-          * constraints we must keep it. *)
-         compare_constraint_type d d' > 0
-       with Not_found ->
-         (** No constraint existing on l *) true) l
-
-exception UpperBoundedAlg
-(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
-   constraints to [lbound], adding them to [cstrs].
-
-    @raise UpperBoundedAlg if any [upper] constraints are strict and
-   [lbound] algebraic. *)
-let enforce_uppers upper lbound cstrs =
-  List.fold_left (fun cstrs (d, r) ->
-      if d == Univ.Le then
-        enforce_leq lbound (Universe.make r) cstrs
-      else
-        match Universe.level lbound with
-        | Some lev -> Constraint.add (lev, d, r) cstrs
-        | None -> raise UpperBoundedAlg)
-    cstrs upper
-
-let minimize_univ_variables ctx us algs left right cstrs =
-  let left, lbounds = 
-    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
-      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
-      else (* Fixed universe, just compute its glb for sharing *)
-        let lbounds =
-	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
-	  | None -> lbounds
-          | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower}
-                                   lbounds
-        in (Univ.LMap.remove r left, lbounds))
-      left (left, Univ.LMap.empty)
-  in
-  let rec instance (ctx, us, algs, insts, cstrs as acc) u =
-    let acc, left, lower =
-      match LMap.find u left with
-      | exception Not_found -> acc, [], LMap.empty
-      | l ->
-	let acc, left, newlow, lower =
-          List.fold_left
-          (fun (acc, left, newlow, lower') (d, l) ->
-           let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in
-	   let l' =
-	     if enf then Universe.make l
-	     else l'
-           in acc', (d, l') :: left,
-              lower_add l d newlow, lower_union lower lower')
-	  (acc, [], LMap.empty, LMap.empty) l
-        in
-        let left = List.uniquize (List.filter (not_lower lower) left) in
-        (acc, left, LMap.union newlow lower)
-    in
-    let instantiate_lbound lbound =
-      let alg = LSet.mem u algs in
-	if alg then
-	  (* u is algebraic: we instantiate it with its lower bound, if any,
-              or enforce the constraints if it is bounded from the top. *)
-          let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in
-          instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc
-	else (* u is non algebraic *)
-	  match Universe.level lbound with
-	  | Some l -> (* The lowerbound is directly a level *) 
-	     (* u is not algebraic but has no upper bounds,
-  	        we instantiate it with its lower bound if it is a 
-	        different level, otherwise we keep it. *)
-             let lower = LMap.remove l lower in
-	     if not (Level.equal l u) then
-	       (* Should check that u does not 
-  	          have upper constraints that are not already in right *)
-               let acc = remove_alg l acc in
-                 instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc
-             else acc, {enforce=true; alg=false; lbound; lower}
-	  | None ->
-            begin match find_inst insts lbound with
-              | can, lower ->
-                (* Another universe represents the same lower bound,
-                   we can share them with no harm. *)
-                let lower = LMap.remove can lower in
-                instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc
-              | exception Not_found ->
-                (* We set u as the canonical universe representing lbound *)
-                instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc
-            end
-    in
-    let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) =
-      match LMap.find u right with
-      | exception Not_found -> acc
-      | upper ->
-        let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in
-        let cstrs = enforce_uppers upper b.lbound cstrs in
-        (ctx, us, algs, insts, cstrs), b
-    in
-    if not (LSet.mem u ctx)
-    then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-    else
-      let lbound = compute_lbound left in
-      match lbound with
-      | None -> (* Nothing to do *)
-        enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower})
-      | Some lbound ->
-        try enforce_uppers (instantiate_lbound lbound)
-        with UpperBoundedAlg ->
-          enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower})
-  and aux (ctx, us, algs, seen, cstrs as acc) u =
-    try acc, LMap.find u seen 
-    with Not_found -> instance acc u
-  in
-    LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) ->
-      if v == None then fst (aux acc u)
-      else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
-      us (ctx, us, algs, lbounds, cstrs)
-
-let normalize_context_set g ctx us algs weak =
-  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
-  (** Keep the Prop/Set <= i constraints separate for minimization *)
-  let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
-  in
-  let smallles = if is_set_minimization ()
-    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
-    else Constraint.empty
-  in
-  let csts, partition =
-    (* We first put constraints in a normal-form: all self-loops are collapsed
-       to equalities. *)
-    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
-			   ctx UGraph.initial_universes
-    in
-    let add_soft u g =
-      if not (Level.is_small u || LSet.mem u ctx)
-      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
-      else g
-    in
-    let g = Constraint.fold
-        (fun (l, d, r) g -> add_soft r (add_soft l g))
-        csts g
-    in
-    let g = UGraph.merge_constraints csts g in
-      UGraph.constraints_of_universes g
-  in
-  (* We ignore the trivial Prop/Set <= i constraints. *)
-  let noneqs =
-    Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
-                           (Level.is_prop l && d == Lt && Level.is_set r)))
-      csts
-  in
-  let noneqs = Constraint.union noneqs smallles in
-  let flex x = LMap.mem x us in
-  let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s ->
-    let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
-    (* Add equalities for globals which can't be merged anymore. *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Eq, g) cst) global
-      cstrs 
-    in
-    (* Also add equalities for rigid variables *)
-    let cstrs = LSet.fold (fun g cst -> 
-      Constraint.add (canon, Eq, g) cst) rigid
-      cstrs
-    in
-    let canonu = Some (Universe.make canon) in
-    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
-      (LSet.diff ctx flexible, us, cstrs))
-    (ctx, us, Constraint.empty) partition
-  in
-  (* Process weak constraints: when one side is flexible and the 2
-     universes are unrelated unify them. *)
-  let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) ->
-      let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
-      let u = norm u and v = norm v in
-      let set_to a b =
-        (LSet.remove a ctx,
-         LMap.add a (Some (Universe.make b)) us,
-         UGraph.enforce_constraint (a,Eq,b) g)
-      in
-      if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u)
-      then acc
-      else
-      if LMap.mem u us
-      then set_to u v
-      else if LMap.mem v us
-      then set_to v u
-      else acc)
-      weak (ctx, us, g)  in
-  (* Noneqs is now in canonical form w.r.t. equality constraints, 
-     and contains only inequality constraints. *)
-  let noneqs =
-    let norm = level_subst_of (normalize_univ_variable_opt_subst us) in
-    Constraint.fold (fun (u,d,v) noneqs ->
-        let u = norm u and v = norm v in
-        if d != Lt && Level.equal u v then noneqs
-        else Constraint.add (u,d,v) noneqs)
-      noneqs Constraint.empty
-  in
-  (* Compute the left and right set of flexible variables, constraints
-     mentionning other variables remain in noneqs. *)
-  let noneqs, ucstrsl, ucstrsr = 
-    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us and rus = LMap.mem r us in
-      let ucstrsl' = 
-	if lus then add_list_map l (d, r) ucstrsl
-	else ucstrsl
-      and ucstrsr' = 
-	add_list_map r (d, l) ucstrsr
-      in 
-      let noneqs = 
-	if lus || rus then noneq 
-	else Constraint.add cstr noneq
-      in (noneqs, ucstrsl', ucstrsr'))
-    noneqs (Constraint.empty, LMap.empty, LMap.empty)
-  in
-  (* Now we construct the instantiation of each variable. *)
-  let ctx', us, algs, inst, noneqs = 
-    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
-  in
-  let us = normalize_opt_subst us in
-    (us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
-
-let is_trivial_leq (l,d,r) =
-  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
-
-(* Prop < i <-> Set+1 <= i <-> Set < i *)
-let translate_cstr (l,d,r as cstr) =
-  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
-    (Level.set, d, r)
-  else cstr
-
-let refresh_constraints univs (ctx, cstrs) =
-  let cstrs', univs' = 
-    Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
-      let c = translate_cstr c in
-      if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
-      cstrs (Univ.Constraint.empty, univs)
-  in ((ctx, cstrs'), univs')
-
-
-(**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
-
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
-
-(*
-   Solve a system of universe constraint of the form
-
-   u_s11, ..., u_s1p1, w1 <= u1
-   ...
-   u_sn1, ..., u_snpn, wn <= un
-
-where
-
-  - the ui (1 <= i <= n) are universe variables,
-  - the sjk select subsets of the ui for each equations,
-  - the wi are arbitrary complex universes that do not mention the ui.
-*)
+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
 
-let is_direct_sort_constraint s v = match s with
-  | Some u -> univ_level_mem u v
-  | None -> false
+(** UnivMinim *)
+module UPairSet = UnivMinim.UPairSet
 
-let solve_constraints_system levels level_bounds level_min =
-  let open Univ in
-  let levels =
-    Array.mapi (fun i o ->
-      match o with
-      | Some u ->
-	(match Universe.level u with 
-	| Some u -> Some u 
-	| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
-      | None -> None)
-      levels in
-  let v = Array.copy level_bounds in
-  let nind = Array.length v in
-  let clos = Array.map (fun _ -> Int.Set.empty) levels in
-  (* First compute the transitive closure of the levels dependencies *)
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
-	clos.(i) <- Int.Set.add j clos.(i);
-    done;
-  done;
-  let rec closure () = 
-    let continue = ref false in
-      Array.iteri (fun i deps -> 
-	let deps' = 
-	  Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
-	in 
-	  if Int.Set.equal deps deps' then ()
-	  else (clos.(i) <- deps'; continue := true))
-	clos;
-      if !continue then closure ()
-      else ()
-  in 
-  closure ();
-  for i=0 to nind-1 do
-    for j=0 to nind-1 do
-      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-    done;
-  done;
-  v
+let normalize_context_set = UnivMinim.normalize_context_set
diff --git a/engine/universes.mli b/engine/universes.mli
index df2e961d6..46ff33a47 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -8,224 +8,231 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Constr
 open Environ
 open Univ
 
-(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
-module UPairSet : CSet.S with type elt = (Level.t * Level.t)
+(** ************************************** *)
+(** This entire module is deprecated. **** *)
+(** ************************************** *)
+[@@@ocaml.warning "-3"]
 
-val set_minimization : bool ref
-val is_set_minimization : unit -> bool
-
-(** Universes *)
+(** ****** Deprecated: moved to [UnivNames] *)
 
 val pr_with_global_universes : Level.t -> Pp.t
+[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
 val reference_of_level : Level.t -> Libnames.reference
+[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
 
-(** Global universe information outside the kernel, to handle
-    polymorphic universes in sections that have to be discharged. *)
 val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
 
 val is_polymorphic : Level.t -> bool
+[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
 
-(** Local universe name <-> level mapping *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
+type universe_binders = UnivNames.universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
 
 val empty_binders : universe_binders
+[@@ocaml.deprecated "Use [UnivNames.empty_binders]"]
 
-val register_universe_binders : GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : GlobRef.t -> universe_binders
-
-type univ_name_list = Misctypes.lname list
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
 
-(** [universe_binders_with_opt_names ref u l]
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
-    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
-    May error if the lengths mismatch.
-
-    Otherwise return [universe_binders_of_global ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
+val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
 
-(** The global universe counter *)
-type universe_id = DirPath.t * int
+(** ****** Deprecated: moved to [UnivGen] *)
 
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+type universe_id = UnivGen.universe_id
+[@@ocaml.deprecated "Use [UnivGen.universe_id]"]
 
-(** Side-effecting functions creating new universe levels. *)
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"]
 
 val new_univ_id : unit -> universe_id
+[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"]
+
 val new_univ_level : unit -> Level.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"]
+
 val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ]"]
+
 val new_Type : unit -> types
+[@@ocaml.deprecated "Use [UnivGen.new_Type]"]
+
 val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"]
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-
-(** {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
+[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"]
 
-(** Build a fresh instance for a given context, its associated substitution and 
-    the instantiated constraints. *)
+val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"]
 
-val fresh_instance_from_context : AUContext.t -> 
+val fresh_instance_from_context : AUContext.t ->
   Instance.t constrained
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"]
 
 val fresh_instance_from : AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"]
 
-val fresh_sort_in_family : env -> Sorts.family -> 
+val fresh_sort_in_family : env -> Sorts.family ->
   Sorts.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"]
+
 val fresh_constant_instance : env -> Constant.t ->
   pconstant in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"]
+
 val fresh_inductive_instance : env -> inductive ->
   pinductive in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"]
+
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"]
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
   constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"]
 
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
   constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"]
 
-(** Get fresh variables for the universe context.
-    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : ContextSet.t -> 
+val fresh_universe_context_set_instance : ContextSet.t ->
   universe_level_subst * ContextSet.t
+[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"]
 
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> GlobRef.t puniverses
+val global_of_constr : constr -> Globnames.global_reference puniverses
+[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"]
 
-val constr_of_global_univ : GlobRef.t puniverses -> constr
+val constr_of_global_univ : Globnames.global_reference puniverses -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"]
 
-val extend_context : 'a in_universe_context_set -> ContextSet.t -> 
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.extend_context]"]
+
+val constr_of_global : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
 
-(** Simplification and pruning of constraints:
-    [normalize_context_set ctx us]
+val constr_of_reference : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
 
-    - Instantiate the variables in [us] with their most precise
-    universe levels respecting the constraints.
+val type_of_global : Globnames.global_reference -> types in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.type_of_global]"]
 
-    - Normalizes the context [ctx] w.r.t. equality constraints, 
-    choosing a canonical universe in each equivalence class 
-    (a global one if there is one) and transitively saturate
-    the constraints w.r.t to the equalities. *)
+(** ****** 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 = Universe.t option universe_map
+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_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 -> 
+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 : 
+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]"]
 
-(** Create a fresh global in the global environment, without side effects.
-    BEWARE: this raises an ANOMALY on polymorphic constants/inductives: 
-    the constraints should be properly added to an evd. 
-    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
-    the proper way to get a fresh copy of a global reference. *)
-val constr_of_global : GlobRef.t -> constr
+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]"]
 
-(** ** DEPRECATED ** synonym of [constr_of_global] *)
-val constr_of_reference : GlobRef.t -> constr
-[@@ocaml.deprecated "synonym of [constr_of_global]"]
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
+[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"]
 
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic 
-    references and computing their instantiated universe context. (side-effect on the
-    universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
+(** ****** Deprecated: moved to [UnivProblem] *)
 
-(** Full universes substitutions into terms *)
+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]"]
 
-val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
-  universe_opt_subst -> constr -> constr
+module Constraints = UnivProblem.Set
+[@@ocaml.deprecated "Use [UnivProblem.Set]"]
 
-val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
+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]"]
 
-(** Pretty-printing *)
+val subst_univs_universe_constraints : universe_subst_fn ->
+  Constraints.t -> Constraints.t
+[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"]
 
-val pr_universe_opt_subst : universe_opt_subst -> Pp.t
+val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
+[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"]
 
-(** {6 Support for template polymorphism } *)
+(** 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]"]
+
+(** ****** Deprecated: moved to [UnivMinim] *)
 
-val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
-  Universe.t array
+module UPairSet = UnivMinim.UPairSet
+[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"]
+
+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
+[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"]
diff --git a/interp/declare.ml b/interp/declare.ml
index c55a6c69b..bc2d2068a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -487,7 +487,7 @@ let add_universe src (dp, i) =
   Option.iter (fun poly ->
       let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
       Global.push_context_set poly ctx;
-      Universes.add_global_universe level poly;
+      UnivNames.add_global_universe level poly;
       if poly then Lib.add_section_context ctx)
     optpoly
 
@@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj =
 
 let declare_univ_binders gr pl =
   if Global.is_polymorphic gr then
-    Universes.register_universe_binders gr pl
+    UnivNames.register_universe_binders gr pl
   else
     let l = match gr with
       | ConstRef c -> Label.to_id @@ Constant.label c
@@ -564,7 +564,7 @@ let do_universe poly l =
   in
   let l =
     List.map (fun {CAst.v=id} ->
-      let lev = Universes.new_univ_id () in
+      let lev = UnivGen.new_univ_id () in
       (id, lev)) l
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
@@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj =
 let do_constraint poly l =
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
-    Universes.is_polymorphic level, level
+    UnivNames.is_polymorphic level, level
   in
   let in_section = Lib.sections_are_opened () in
   let () =
diff --git a/interp/declare.mli b/interp/declare.mli
index de4d8346a..4a9f54278 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) ->
 val exists_name : Id.t -> bool
 
 (** Global universe contexts, names and constraints *)
-val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index a09abfa19..7f98ed427 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -2,11 +2,11 @@ let contrib_name = "btauto"
 
 let init_constant dir s =
   let find_constant contrib dir s =
-    Universes.constr_of_global (Coqlib.find_reference contrib dir s)
+    UnivGen.constr_of_global (Coqlib.find_reference contrib dir s)
   in
   find_constant contrib_name dir s
 
-let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
+let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
 
 let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f25f63624..cdd698304 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
+           let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in
 	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
            let ar = EConstr.of_constr ar in
            let info = (fst (flag_of_type env sg ar) = Info) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 2d7a3e37b..b13580bc0 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -233,7 +233,7 @@ let ll_forall_tac prod backtrack id continue seq=
 
 (* special for compatibility with old Intuition *)
 
-let constant str = Universes.constr_of_global
+let constant str = UnivGen.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 0ea70c19f..96be1d893 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -283,15 +283,15 @@ let fourier_lineq lineq1 =
 let get = Lazy.force
 let cget = get
 let eget c = EConstr.of_constr (Lazy.force c)
-let constant path s = Universes.constr_of_global @@
+let constant path s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "Fourier" path s
 
 (* Standard library *)
 open Coqlib
 let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ())
-let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ())
-let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ())
+let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ())
+let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ())
+let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ())
 
 (* Rdefinitions *)
 let constant_real = constant ["Reals";"Rdefinitions"]
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 44fa0740d..3801fec4b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in
-  let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in
-  let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in
+  let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in
+  let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in
+  let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1603,7 +1603,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
      | Value lemma -> EConstr.of_constr lemma
-     | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ())
+     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ())
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index dc0f240bd..a158fc8ff 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -689,7 +689,7 @@ let build_case_scheme fa =
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
-       Universes.new_sort_in_family x
+       UnivGen.new_sort_in_family x
     )
       fa
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a0b9217c7..35c3acd41 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -117,7 +117,7 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
@@ -471,7 +471,7 @@ let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -479,7 +479,7 @@ let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -492,7 +492,7 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
 let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
 
-let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 094f54156..180952635 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
+    EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
   with _ -> assert false 
 
 	  
@@ -512,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
+                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENLIST[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2a3a85fcc..2464c595f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -49,7 +49,7 @@ open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
 
-let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
   Coqlib.coq_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Arith";"PeanoNat";"Nat"]
@@ -61,7 +61,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 
 let find_reference sl s =
@@ -1241,7 +1241,7 @@ let get_current_subgoals_types () =
 
 exception EmptySubgoals
 let build_and_l sigma l =
-  let and_constr =  Universes.constr_of_global @@ Coqlib.build_coq_and () in
+  let and_constr =  UnivGen.constr_of_global @@ Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 168105e8f..4c0357dd8 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -373,7 +373,7 @@ struct
     * ZMicromega.v
     *)
 
-  let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+  let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
   let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 81b44ffad..d2d4639d2 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -136,7 +136,7 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let gen_constant msg path s = Universes.constr_of_global @@
+let gen_constant msg path s = UnivGen.constr_of_global @@
   coq_reference msg path s
 
 let tpexpr  = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 51cd665f6..e455ebb28 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -206,7 +206,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
+let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 912429c31..7464b42dc 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -120,7 +120,7 @@ open Proofview.Notations
   the constants are loaded in the environment *)
 
 let constant dir s =
-  EConstr.of_constr @@ Universes.constr_of_global @@
+  EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "Quote" ("quote"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index ad3afafd8..949cba2db 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -69,19 +69,19 @@ let z_module = [["Coq";"ZArith";"BinInt"]]
 
 let init_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
 let constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" coq_modules x
 let z_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" z_module x
 let bin_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" bin_module x
 
 (* Logic *)
@@ -170,7 +170,7 @@ let mk_list univ typ l =
   loop l
 
 let mk_plist =
-  let type1lev = Universes.new_univ_level () in
+  let type1lev = UnivGen.new_univ_level () in
   fun l -> mk_list type1lev EConstr.mkProp l
 
 let mk_list = mk_list Univ.Level.set
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 946b6dff4..8a0f48dc4 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -26,27 +26,27 @@ let step_count = ref 0
 
 let node_count = ref 0
 
-let logic_constant s = Universes.constr_of_global @@
+let logic_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
 
 let li_False = lazy (destInd (logic_constant "False"))
 let li_and   = lazy (destInd (logic_constant "and"))
 let li_or    = lazy (destInd (logic_constant "or"))
 
-let pos_constant s = Universes.constr_of_global @@
+let pos_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
 let l_xH = lazy (pos_constant "xH")
 
-let store_constant s = Universes.constr_of_global @@
+let store_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
 
 let l_empty = lazy (store_constant "empty")
 let l_push = lazy (store_constant "push")
 
-let constant s = Universes.constr_of_global @@
+let constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
 
 let l_Reflect = lazy (constant "Reflect")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 074fcb92e..59ba4b7de 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -105,7 +105,7 @@ let protect_tac_in map id =
 let closed_term t l =
   let open Quote_plugin in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let l = List.map Universes.constr_of_global l in
+  let l = List.map UnivGen.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 
@@ -233,7 +233,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -279,7 +279,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
@@ -927,7 +927,7 @@ let ftheory_to_obj : field_info -> obj =
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
-        let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in
+        let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in
         let c = EConstr.of_constr c in
         mkApp(c,[|r;r;inv|])
     | _ ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e9e045a53..c0026616d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1221,7 +1221,7 @@ let genclrtac cl cs clr =
       (fun type_err gl ->
          tclTHEN
            (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
-             (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
+             (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
            (fun gl -> raise type_err)
            gl))
     (old_cleartac clr)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 7d7655d29..a31022919 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -435,7 +435,7 @@ let lz_setoid_relation =
   | env', srel when env' == env -> srel
   | _ ->
     let srel =
-       try Some (Universes.constr_of_global @@
+       try Some (UnivGen.constr_of_global @@
                    Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation")
        with _ -> None in
     last_srel := (env, srel); srel
@@ -482,7 +482,7 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then
+        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index afa8a12fc..7dbef01c2 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -316,7 +316,7 @@ let lookup_pattern_path_between env (s,t) =
 
 let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; 
 		     coe_is_identity = b; coe_is_projection = b' } =
-  let subst, ctx = Universes.fresh_universe_context_set_instance ctx in
+  let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in
   let c' = Vars.subst_univs_level_constr subst c 
   and t' = Vars.subst_univs_level_constr subst t in
     (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
@@ -440,7 +440,7 @@ let cache_coercion env sigma (_, c) =
   let () = add_class c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
-  let value, ctx = Universes.fresh_global_instance env c.coercion_type in
+  let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in
   let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
   let typ = EConstr.Unsafe.to_constr typ in
   let xf =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 49c429458..062136ff5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option {
 (* XXX: we would like to search for this with late binding
    "data.id.type" etc... *)
 let impossible_default_case () =
-  let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+  let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
   let (_, u) = Constr.destConst c in
   Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
 
@@ -210,7 +210,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let u, ctx' = Universes.fresh_instance_from ctx None in
+  let u, ctx' = UnivGen.fresh_instance_from ctx None in
   let subst = Univ.make_inverse_instance_subst u in
   let c = EConstr.of_constr c in
   let c' = subst_univs_level_constr subst c in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 3327c250d..40f4d4ff8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
     if not (Sorts.List.mem kind (elim_sorts specif)) then
       raise
 	(RecursionSchemeError
-	   (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
+           (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind)))
   in
   let ndepar = mip.mind_nrealdecls + 1 in
 
@@ -550,7 +550,7 @@ let check_arities env listdepkind =
        let kelim = elim_sorts (mibi,mipi) in
        if not (Sorts.List.mem kind kelim) then raise
 	 (RecursionSchemeError
-	  (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env
+          (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env
 					      kind),(mind,u))))
        else if Int.List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 616ccf0cf..6bf852fcd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -169,14 +169,6 @@ let _ =
 	    optread  = is_strict_universe_declarations;
 	    optwrite = (:=) strict_universe_declarations })
 
-let _ =
-  Goptions.(declare_bool_option
-	  { optdepr  = false;
-	    optname  = "minimization to Set";
-	    optkey   = ["Universe";"Minimization";"ToSet"];
-	    optread  = Universes.is_set_minimization;
-	    optwrite = (:=) Universes.set_minimization })
-
 (** Miscellaneous interpretation functions *)
 
 let interp_known_universe_level evd r =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a4d447902..34d7a0798 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -83,7 +83,7 @@ let declare_reduction_effect funkey f =
 
 (** A function to set the value of the print function *)
 let set_reduction_effect x funkey =
-  let termkey = Universes.constr_of_global x in
+  let termkey = UnivGen.constr_of_global x in
   Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey))
 
 
@@ -701,18 +701,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
 let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
-    let open Universes in
+    let open UnivProblem in
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
-      let (cst, u), ctx = fresh_constant_instance env cst in
+      let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
         let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
-          let subst = Constraints.fold (fun cst acc ->
+          let subst = Set.fold (fun cst acc ->
               let l, r = match cst with
                 | ULub (u, v) | UWeak (u, v) -> u, v
                 | UEq (u, v) | ULe (u, v) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4386144fe..11cc6c1f0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -281,7 +281,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
   let ty, ctx = Global.type_of_global_in_context env glob in
-  let inst, ctx = Universes.fresh_instance_from ctx None in
+  let inst, ctx = UnivGen.fresh_instance_from ctx None in
   let ty = Vars.subst_instance_constr inst ty in
   let ty = EConstr.of_constr ty in
   let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
@@ -321,7 +321,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
-  let term = Universes.constr_of_global_univ (glob, inst) in
+  let term = UnivGen.constr_of_global_univ (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1caa629ff..62bee5a36 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -561,16 +561,16 @@ let is_rigid_head sigma flags t =
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
-  let open Universes in
-  Constraints.fold
+  let open UnivProblem in
+  Set.fold
     (fun c acc ->
        let c' = match c with
          (* Should we be forcing weak constraints? *)
          | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
          | ULe _ | UEq _ -> c
        in
-        Constraints.add c' acc)
-    c Constraints.empty
+        Set.add c' acc)
+    c Set.empty
 
 let constr_cmp pb env sigma flags t u =
   let cstrs =
@@ -1504,8 +1504,7 @@ let indirectly_dependent sigma c d decls =
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
-  let sigma, subst = nf_univ_variables sigma in
-  (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+  (sigma, nf_evar sigma c)
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1593,9 +1592,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
-     let univs, subst = nf_univ_variables sigma in
-     Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+     let c = applist (local_strong whd_meta sigma c, l) in
+     Some (sigma, c))
 
 let make_eq_test env evd c =
   let out cstr =
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index e15c3ad04..304a5dadd 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -32,8 +32,8 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
-type univ_name_list = Universes.univ_name_list
-[@@ocaml.deprecated "Use [Universes.univ_name_list]"]
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
 type printable =
   | PrintTables
@@ -49,7 +49,7 @@ type printable =
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation * Universes.univ_name_list option
+  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
@@ -65,7 +65,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option
+  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 185b1648c..d036fec21 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,8 +35,8 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
@@ -93,7 +93,7 @@ let print_ref reduce ref udecl =
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
-  let bl = Universes.universe_binders_with_opt_names ref
+  let bl = UnivNames.universe_binders_with_opt_names ref
       (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let inst =
@@ -594,7 +594,7 @@ let print_constant with_values sep sp udecl =
   in
   let ctx =
     UState.of_binders
-      (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+      (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 2f2dcd563..50042d6c5 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -34,10 +34,10 @@ val print_eval :
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
 val print_name : env -> Evd.evar_map -> reference or_by_notation ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
 val print_about : env -> Evd.evar_map -> reference or_by_notation ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
@@ -84,8 +84,8 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+  print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index edcce874d..77466605a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_global = pr_global_env Id.Set.empty
 let pr_puniverses f env (c,u) =
   f env c ++ 
   (if !Constrextern.print_universes then
-    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+    str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
    else mt ())
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f3..3c805b327 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -140,7 +140,7 @@ let print_mutual_inductive env mind mib udecl =
                        (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
     else []
   in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -183,7 +183,7 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
       (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0b0b0a35..48ba866cc 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool
 
 val pr_mutual_inductive_body : Environ.env ->
   MutInd.t -> Declarations.mutual_inductive_body ->
-  Universes.univ_name_list option -> Pp.t
+  UnivNames.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 842003bc8..97cfccb8d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -342,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
      normalise them for the kernel. *)
   let subst_evar k =
     Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
-  let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
   let make_body =
     if poly || now then
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c1d69dfc5..092bb5c27 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_ids_set_of_hyps gls =
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 85a7f1495..768d94d30 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Universes.universe_id list
+    | MoreDataUnivLevel of UnivGen.universe_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
@@ -171,7 +171,7 @@ module Make(T : Task) () = struct
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init n (fun _ -> Universes.new_univ_id ()) in
+      CList.init n (fun _ -> UnivGen.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -310,7 +310,7 @@ module Make(T : Task) () = struct
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
     (* We ask master to allocate universe identifiers *)
-    Universes.set_remote_new_univ_id (bufferize (fun () ->
+    UnivGen.set_remote_new_univ_id (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
       | MoreDataUnivLevel l -> l));
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 15a24fb37..77fe31415 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -79,7 +79,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
-      let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       (** Only metas are mentioning the old universes. *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b8..627ac31f5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
   let try_rewrite dir ctx c tc =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+    let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bbcf8def6..ea5d4719c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
   Refine.refine ~typecheck:false begin fun sigma ->
       let sigma, term, ty =
         if poly then
-          let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+          let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
           let map c = Vars.subst_univs_level_constr subst c in
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
           sigma, map c, map t
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2408b8f2b..3df9e3f82 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -89,7 +89,7 @@ let rec prolog l n gl =
 
 let out_term env = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+  | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de6452..715686ad0 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -102,7 +102,7 @@ let get_coq_eq ctx =
     let eq = Globnames.destIndRef Coqlib.glob_eq in
     (* Do not force the lazy if they are not defined *)
     let eq, ctx = with_context_set ctx 
-      (Universes.fresh_inductive_instance (Global.env ()) eq) in
+      (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
       mkIndU eq, mkConstructUi (eq,1), ctx
   with Not_found ->
     user_err Pp.(str "eq not found.")
@@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) =
 (**********************************************************************)
 
 let build_sym_scheme env ind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
@@ -241,11 +241,11 @@ let sym_scheme_kind =
 let const_of_scheme kind env ind ctx = 
   let sym_scheme, eff = (find_scheme kind ind) in
   let sym, ctx = with_context_set ctx 
-    (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+    (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
     mkConstU sym, ctx, eff
 
 let build_sym_involutive_scheme env ind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
@@ -353,7 +353,7 @@ let sym_involutive_scheme_kind =
 (**********************************************************************)
 
 let build_l2r_rew_scheme dep env ind kind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
@@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind =
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let build_l2r_forward_rew_scheme dep env ind kind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n p =
@@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let realsign_ind_P n aP =
     name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let build_r2l_forward_rew_scheme dep env ind kind = 
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
@@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -755,7 +755,7 @@ let rew_r2l_scheme_kind =
 
 let build_congr env (eq,refl,ctx) ind =
   let (ind,u as indu), ctx = with_context_set ctx 
-    (Universes.fresh_inductive_instance env ind) in
+    (UnivGen.fresh_inductive_instance env ind) in
   let (mib,mip) = lookup_mind_specif env ind in
   if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
@@ -778,7 +778,7 @@ let build_congr env (eq,refl,ctx) ind =
   let varH = fresh env (Id.of_string "H") in
   let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
-  let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+  let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
   let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d142e10a4..8904cd170 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1781,7 +1781,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
         let u = EInstance.kind sigma u in
-        let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+        let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
@@ -1832,7 +1832,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
       let u = EInstance.kind sigma u in
-      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+      let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d02bab186..39034a19b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
     | IsGlobRef gr ->
-      let (c, ctx) = Universes.fresh_global_instance env gr in
+      let (c, ctx) = UnivGen.fresh_global_instance env gr in
        true, (EConstr.of_constr c, ctx)
     | IsConstr (c, ctx) -> false, (c, ctx)
   in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 62ead57f3..6d0da0dfa 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,7 +123,7 @@ let define internal id c p univs =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
-  let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in
+  let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs =
     if p then Polymorphic_const_entry (UState.context ctx)
     else Monomorphic_const_entry (UState.context_set ctx)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5e602289b..2a41a50dd 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -59,15 +59,15 @@ exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
 
-let constr_of_global g = lazy (Universes.constr_of_global g)
+let constr_of_global g = lazy (UnivGen.constr_of_global g)
 
 (* Some pre declaration of constant we are going to use *)
 let bb = constr_of_global Coqlib.glob_bool
 
-let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
 
 let andb_true_intro = fun _ ->
-  Universes.constr_of_global
+  UnivGen.constr_of_global
     (Coqlib.build_bool_type()).Coqlib.andb_true_intro
 
 let tt = constr_of_global Coqlib.glob_true
@@ -76,9 +76,9 @@ let ff = constr_of_global Coqlib.glob_false
 
 let eq = constr_of_global Coqlib.glob_eq
 
-let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ())
+let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ())
 
-let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c = induction false None c None None
 
@@ -863,7 +863,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
             mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
-              mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
+              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
           )
         )
       )
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1ac597695..61ce5d6c4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -423,13 +423,13 @@ let context poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus = match b with
       | None ->
-        pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
+        pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let hook = Lemmas.mk_hook (fun _ gr -> gr) in
-        let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
+        let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 26a46a752..722f21171 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -174,7 +174,7 @@ let do_assumptions kind nl l =
       let t = replace_vars subst t in
       let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
-          (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+          (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
           idl refs
       in
       subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2f2c7c4e2..56932360a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind ->
   types in_constant_universes_entry ->
-  Universes.universe_binders -> Impargs.manual_implicits ->
+  UnivNames.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
   GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b2532485a..629fcce5a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -177,6 +177,72 @@ let is_flexible_sort evd u =
   | Some l -> Evd.is_flexible_level evd l
   | None -> false
 
+(**********************************************************************)
+(* Tools for template polymorphic inductive types                         *)
+
+(* Miscellaneous functions to remove or test local univ assumed to
+   occur only in the le constraints *)
+
+(*
+   Solve a system of universe constraint of the form
+
+   u_s11, ..., u_s1p1, w1 <= u1
+   ...
+   u_sn1, ..., u_snpn, wn <= un
+
+where
+
+  - the ui (1 <= i <= n) are universe variables,
+  - the sjk select subsets of the ui for each equations,
+  - the wi are arbitrary complex universes that do not mention the ui.
+*)
+
+let is_direct_sort_constraint s v = match s with
+  | Some u -> Univ.univ_level_mem u v
+  | None -> false
+
+let solve_constraints_system levels level_bounds =
+  let open Univ in
+  let levels =
+    Array.mapi (fun i o ->
+      match o with
+      | Some u ->
+        (match Universe.level u with
+        | Some u -> Some u
+        | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
+      | None -> None)
+      levels in
+  let v = Array.copy level_bounds in
+  let nind = Array.length v in
+  let clos = Array.map (fun _ -> Int.Set.empty) levels in
+  (* First compute the transitive closure of the levels dependencies *)
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
+        clos.(i) <- Int.Set.add j clos.(i);
+    done;
+  done;
+  let rec closure () =
+    let continue = ref false in
+      Array.iteri (fun i deps ->
+        let deps' =
+          Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
+        in
+          if Int.Set.equal deps deps' then ()
+          else (clos.(i) <- deps'; continue := true))
+        clos;
+      if !continue then closure ()
+      else ()
+  in
+  closure ();
+  for i=0 to nind-1 do
+    for j=0 to nind-1 do
+      if not (Int.equal i j) && Int.Set.mem j clos.(i) then
+        (v.(i) <- Universe.sup v.(i) level_bounds.(j));
+    done;
+  done;
+  v
+
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
@@ -205,8 +271,8 @@ let inductive_levels env evd poly arities inds =
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
-  let levels' = Universes.solve_constraints_system (Array.of_list levels)
-    (Array.of_list cstrs_levels) (Array.of_list min_levels)
+  let levels' = solve_constraints_system (Array.of_list levels)
+    (Array.of_list cstrs_levels)
   in
   let evd, arities =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 833935724..7ae8e8f71 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -37,7 +37,7 @@ type one_inductive_impls =
   Impargs.manual_implicits list (** for constrs *)
 
 val declare_mutual_inductive_with_eliminations :
-  mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
+  mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
   MutInd.t
 
 (** Exported for Funind *)
@@ -64,4 +64,4 @@ val extract_mutual_inductive_declaration_components :
 val interp_mutual_inductive :
   structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
   polymorphic -> private_flag -> Declarations.recursivity_kind ->
-  mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+  mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 349fc562b..f41e0fc44 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         (** FIXME: include locality *)
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
-        let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
+        let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 12973f51b..c5e704a5e 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,11 +14,11 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition : Id.t -> definition_kind ->
-  Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+  Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
     GlobRef.t Lemmas.declaration_hook -> GlobRef.t
 
 val declare_fix : ?opaque:bool -> definition_kind ->
-  Universes.universe_binders -> Entries.constant_universes_entry ->
+  UnivNames.universe_binders -> Entries.constant_universes_entry ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
   GlobRef.t
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f9167f969..f68dcae26 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -55,7 +55,7 @@ let process_vernac_interp_error exn = match fst exn with
     let msg =
       if !Constrextern.print_universes then
 	str "." ++ spc() ++ 
-	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
+          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
       else
 	mt() in
     wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index acb461cac..3c4fcf714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -197,7 +197,7 @@ let rec pr_disjunction pr = function
 let pr_puniverses f env (c,u) = 
   f env c ++ 
   (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
-    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+    str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
   else mt())
 
 let explain_elim_arity env sigma ind sorts c pj okinds =
@@ -314,7 +314,7 @@ let explain_unification_error env sigma p1 p2 = function
      | UnifUnivInconsistency p ->
         if !Constrextern.print_universes then
 	  [str "universe inconsistency: " ++
-          Univ.explain_universe_inconsistency Universes.pr_with_global_universes p]
+          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
 	else
           [str "universe inconsistency"]
      | CannotSolveConstraint ((pb,env,t,u),e) ->
@@ -886,7 +886,7 @@ let explain_not_match_error = function
     str"polymorphic universe instances do not match"
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
-      Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon
+      Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
   | IncompatiblePolymorphism (env, t1, t2) ->
     str "conversion of polymorphic values generates additional constraints: " ++
       quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 32885ab88..2deca1e06 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort =
 	 match inst with
 	 | None ->
 	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
-	    let u, ctx = Universes.fresh_instance_from ctx None in
+            let u, ctx = UnivGen.fresh_instance_from ctx None in
             let evd = Evd.from_ctx (UState.of_context_set ctx) in
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ae1065ef5..1e7721f8f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty =
 let tactics_module = ["Program";"Tactics"]
 let safe_init_constant md name () =
   Coqlib.check_required_library ("Coq"::md);
-  Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
+  UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
 let hide_obligation = safe_init_constant tactics_module "obligation"
 
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
@@ -472,7 +472,7 @@ let subst_body expand prg =
 
 let declare_definition prg =
   let body, typ = subst_body true prg in
-  let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
     (UState.subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
@@ -555,7 +555,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let univs = UState.const_univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
-  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
+  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
diff --git a/vernac/record.ml b/vernac/record.ml
index b0f229294..bf6affd5f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -316,7 +316,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
                 let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
                 let kn = destConstRef gr in
                 Declare.definition_message fid;
-                Universes.register_universe_binders gr ubinders;
+                UnivNames.register_universe_binders gr ubinders;
                 kn, mkProj (Projection.make kn false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
@@ -352,7 +352,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 		      applist (mkConstU (kn,u),proj_args) 
                   in
                   Declare.definition_message fid;
-                  Universes.register_universe_binders (ConstRef kn) ubinders;
+                  UnivNames.register_universe_binders (ConstRef kn) ubinders;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
@@ -465,9 +465,9 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref [paramimpls];
-      Universes.register_universe_binders cref ubinders;
+      UnivNames.register_universe_binders cref ubinders;
       Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
-      Universes.register_universe_binders (ConstRef proj_cst) ubinders;
+      UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
 	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
diff --git a/vernac/record.mli b/vernac/record.mli
index 308c9e9b9..b2c039f0b 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,7 @@ val declare_projections :
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
   bool list ->
-  Universes.universe_binders ->
+  UnivNames.universe_binders ->
   Impargs.manual_implicits list ->
   Context.Rel.t ->
     (Name.t * bool) list * Constant.t option list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 938e9718a..eae8167c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1741,7 +1741,7 @@ let vernac_print ~atts env sigma =
        else str"There may remain asynchronous universe constraints"
      in
      begin match dst with
-     | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining
+     | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
      | Some s -> dump_universes_gen univ s
      end
   | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)