Merge PR #6893: Cleanup UState API usage

24 files changed, 103 insertions, 81 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 7674cf67a..6b3ce048f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -89,15 +89,15 @@ let nf_evars_universes evm =
     (Evd.universe_subst evm)
     
 let nf_evars_and_universes evm =
-  let evm = Evd.nf_constraints evm in
+  let evm = Evd.minimize_universes evm in
     evm, nf_evars_universes evm
 
 let e_nf_evars_and_universes evdref =
-  evdref := Evd.nf_constraints !evdref;
+  evdref := Evd.minimize_universes !evdref;
   nf_evars_universes !evdref, Evd.universe_subst !evdref
 
 let nf_evar_map_universes evm =
-  let evm = Evd.nf_constraints evm in
+  let evm = Evd.minimize_universes evm in
   let subst = Evd.universe_subst evm in
     if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
diff --git a/engine/evd.ml b/engine/evd.ml
index e7d542d12..185cab101 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -253,21 +253,8 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-type evar_universe_context = UState.t
 
-type 'a in_evar_universe_context = 'a * evar_universe_context
-
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let add_universe_constraints_context = UState.add_universe_constraints
-let constrain_variables = UState.constrain_variables 
-let evar_universe_context_of_binders = UState.of_binders
+type 'a in_evar_universe_context = 'a * UState.t
 
 (*******************************************************************)
 (* Metamaps *)
@@ -427,7 +414,7 @@ type evar_map = {
   undf_evars : evar_info EvMap.t;
   evar_names : EvNames.t;
   (** Universes *)
-  universes  : evar_universe_context;
+  universes  : UState.t;
   (** Conversion problems *)
   conv_pbs   : evar_constraint list;
   last_mods  : Evar.Set.t;
@@ -558,10 +545,10 @@ let existential_type d (n, args) =
   instantiate_evar_array info info.evar_concl args
 
 let add_constraints d c =
-  { d with universes = add_constraints_context d.universes c }
+  { d with universes = UState.add_constraints d.universes c }
 
 let add_universe_constraints d c = 
-  { d with universes = add_universe_constraints_context d.universes c }
+  { d with universes = UState.add_universe_constraints d.universes c }
 
 (*** /Lifting... ***)
 
@@ -586,7 +573,7 @@ let create_evar_defs sigma = { sigma with
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
-  universes  = empty_evar_universe_context;
+  universes  = UState.empty;
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
@@ -609,14 +596,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
   let universes = 
     if not with_univs then evd.universes
-    else union_evar_universe_context evd.universes d.universes
+    else UState.union evd.universes d.universes
   in
   { evd with
     metas = d.metas;
     last_mods; conv_pbs; universes }
 
 let merge_universe_context evd uctx' =
-  { evd with universes = union_evar_universe_context evd.universes uctx' }
+  { evd with universes = UState.union evd.universes uctx' }
 
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
@@ -798,16 +785,6 @@ let make_flexible_variable evd ~algebraic u =
   { evd with universes =
       UState.make_flexible_variable evd.universes ~algebraic u }
 
-let make_evar_universe_context e l =
-  let uctx = UState.make (Environ.universes e) in
-  match l with
-  | None -> uctx
-  | Some us ->
-      List.fold_left
-        (fun uctx { CAst.loc; v = id } ->
-        fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
-        uctx us
-
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -910,10 +887,6 @@ let check_eq evd s s' =
 let check_leq evd s s' =
   UGraph.check_leq (UState.ugraph evd.universes) s s'
 
-let normalize_evar_universe_context_variables = UState.normalize_variables
-
-let abstract_undefined_variables = UState.abstract_undefined_variables
-
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
@@ -922,16 +895,14 @@ let refresh_undefined_universes evd =
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let normalize_evar_universe_context = UState.normalize
-
-let nf_univ_variables evd = 
-  let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
+let nf_univ_variables evd =
+  let subst, uctx' = UState.normalize_variables evd.universes in
   let evd' = {evd with universes = uctx'} in
     evd', subst
 
-let nf_constraints evd =
-  let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
-  let uctx' = normalize_evar_universe_context uctx' in
+let minimize_universes evd =
+  let subst, uctx' = UState.normalize_variables evd.universes in
+  let uctx' = UState.minimize uctx' in
     {evd with universes = uctx'}
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
@@ -1076,7 +1047,7 @@ let clear_metas evd = {evd with metas = Metamap.empty}
 let meta_merge ?(with_univs = true) evd1 evd2 =
   let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
   let universes =
-    if with_univs then union_evar_universe_context evd2.universes evd1.universes
+    if with_univs then UState.union evd2.universes evd1.universes
     else evd2.universes
   in
   {evd2 with universes; metas; }
@@ -1176,3 +1147,25 @@ module Monad =
 (* Failure explanation *)
 
 type unsolvability_explanation = SeveralInstancesFound of int
+
+(** Deprecated *)
+type evar_universe_context = UState.t
+let empty_evar_universe_context = UState.empty
+let union_evar_universe_context = UState.union
+let evar_universe_context_set = UState.context_set
+let evar_universe_context_constraints = UState.constraints
+let evar_context_universe_context = UState.context
+let evar_universe_context_of = UState.of_context_set
+let evar_universe_context_subst = UState.subst
+let add_constraints_context = UState.add_constraints
+let constrain_variables = UState.constrain_variables
+let evar_universe_context_of_binders = UState.of_binders
+let make_evar_universe_context e l =
+  let g = Environ.universes e in
+  match l with
+  | None -> UState.make g
+  | Some l -> UState.make_with_initial_binders g l
+let normalize_evar_universe_context_variables = UState.normalize_variables
+let abstract_undefined_variables = UState.abstract_undefined_variables
+let normalize_evar_universe_context = UState.minimize
+let nf_constraints = minimize_universes
diff --git a/engine/evd.mli b/engine/evd.mli
index ed3316c16..49c953f6d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,22 +493,31 @@ val univ_flexible_alg : rigid
 type 'a in_evar_universe_context = 'a * UState.t
 
 val evar_universe_context_set : UState.t -> Univ.ContextSet.t
+[@@ocaml.deprecated "Alias of UState.context_set"]
 val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
+[@@ocaml.deprecated "Alias of UState.constraints"]
 val evar_context_universe_context : UState.t -> Univ.UContext.t
 [@@ocaml.deprecated "alias of UState.context"]
 
 val evar_universe_context_of : Univ.ContextSet.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.of_context_set"]
 val empty_evar_universe_context : UState.t
+[@@ocaml.deprecated "Alias of UState.empty"]
 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
+[@@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
+[@@ocaml.deprecated "Alias of UState.of_binders"]
 
 val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
+[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
 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
@@ -516,13 +525,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 val universe_binders : evar_map -> Universes.universe_binders
 val add_constraints_context : UState.t ->
   Univ.Constraint.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.add_constraints"]
 
 
 val normalize_evar_universe_context_variables : UState.t -> 
   Univ.universe_subst in_evar_universe_context
+[@@ocaml.deprecated "Alias of UState.normalize_variables"]
 
-val normalize_evar_universe_context : UState.t -> 
-  UState.t
+val normalize_evar_universe_context : UState.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.minimize"]
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
 val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -581,12 +592,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : UState.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
 
 val fix_undefined_variables : evar_map -> evar_map
 
 val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
 
+(** Universe minimization *)
+val minimize_universes : evar_map -> evar_map
 val nf_constraints : evar_map -> evar_map
+[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
 
 val update_sigma_env : evar_map -> env -> evar_map
 
diff --git a/engine/termops.ml b/engine/termops.ml
index c615155d1..35258762a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont
 
 let pr_evar_universe_context ctx =
   let open UState in
-  let open Evd in
   let prl = pr_uctx_level ctx in
   if UState.is_empty ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
diff --git a/engine/uState.ml b/engine/uState.ml
index 00825208b..e57afd743 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name
                 uctx_initial_universes = initial}
   in uctx', u
 
+let make_with_initial_binders e us =
+  let uctx = make e in
+  List.fold_left
+    (fun uctx { CAst.loc; v = id } ->
+       fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
+    uctx us
+
 let add_global_univ uctx u =
   let initial =
     UGraph.add_universe u true uctx.uctx_initial_universes
@@ -578,7 +585,7 @@ let refresh_undefined_univ_variables uctx =
                uctx_initial_universes = initial } in
     uctx', subst
 
-let normalize uctx = 
+let minimize uctx =
   let ((vars',algs'), us') = 
     Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
 				    uctx.uctx_univ_algebraic
@@ -606,3 +613,6 @@ let update_sigma_env uctx env =
                          uctx_universes = univs }
   in
   merge true univ_rigid eunivs eunivs.uctx_local
+
+(** Deprecated *)
+let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 68fe350c0..9a2bc706b 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,6 +26,8 @@ val empty : t
 
 val make : UGraph.t -> t
 
+val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+
 val is_empty : t -> bool
 
 val union : t -> t -> t
@@ -131,7 +133,10 @@ val fix_undefined_variables : t -> t
 
 val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
+(** Universe minimization *)
+val minimize : t -> t
 val normalize : t -> t
+[@@ocaml.deprecated "Alias of UState.minimize"]
 
 type universe_decl =
   (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6e38b4641..e0368153e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m =
   in
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
-  let evd = Evd.nf_constraints evd in
+  let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
   Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 43c29a08a..f049963f1 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1193,7 +1193,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
     else let gl, ccl =  pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl
   else if to_ind && occ = None then
     let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in
-    let ucst = Evd.union_evar_universe_context ucst ucst' in
+    let ucst = UState.union ucst ucst' in
     if nv = 0 then anomaly "occur_existential but no evars" else
     let gl, pty = pfe_type_of gl p in
     false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 859513d5c..57635edac 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -216,7 +216,7 @@ let same_proj sigma t1 t2 =
 let all_ok _ _ = true
 
 let fake_pmatcher_end () =
-  mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp)
+  mkProp, L2R, (Evd.empty, UState.empty, mkProp)
 
 let unfoldintac occ rdx t (kt,_) gl = 
   let fs sigma x = Reductionops.nf_evar sigma x in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 62c35d6df..33b18001c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -361,7 +361,7 @@ let unif_end env sigma0 ise0 pt ok =
   if ise2 == ise1 then (s, uc, t)
   else
     let s, uc', t = nf_open_term sigma0 ise2 t in
-    s, Evd.union_evar_universe_context uc uc', t
+    s, UState.union uc uc', t
 
 let unify_HO env sigma0 t1 t2 =
   let sigma = unif_HO env sigma0 t1 t2 in
@@ -1268,7 +1268,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
     let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in
     sigma, [pat] in
   match pattern with
-  | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context
+  | None -> do_subst env0 concl0 concl0 1, UState.empty
   | Some (sigma, (T rp | In_T rp)) -> 
     let rp = fs sigma rp in
     let ise = create_evar_defs sigma in
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index d16f046fa..8864be576 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -38,7 +38,7 @@ let interp_univ_constraints env evd cstrs =
 let interp_univ_decl env decl =
   let open Misctypes in
   let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
+  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = { univdecl_instance = pl;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 3682b7c25..9da94e42a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -94,7 +94,7 @@ let print_ref reduce ref udecl =
   let env = Global.env () in
   let bl = Universes.universe_binders_with_opt_names ref
       (Array.to_list (Univ.Instance.to_array inst)) udecl in
-  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
   let inst =
     if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
     else mt ()
@@ -593,7 +593,7 @@ let print_constant with_values sep sp udecl =
         Array.to_list (Instance.to_array inst)
   in
   let ctx =
-    Evd.evar_universe_context_of_binders
+    UState.of_binders
       (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 43796ec61..e076c10f3 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -141,7 +141,7 @@ let print_mutual_inductive env mind mib udecl =
     else []
   in
   let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
-  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
            (Declareops.inductive_is_polymorphic mib) 
@@ -185,7 +185,7 @@ let print_record env mind mib udecl =
   let envpar = push_rel_context params env in
   let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
       (Array.to_list (Univ.Instance.to_array u)) udecl in
-  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
     let open Declarations in
     match mib.mind_finite with
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d713b0999..8b5b739a3 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -341,7 +341,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let subst_evar k =
     Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in
   let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
-    (Evd.evar_universe_context_subst universes) in
+    (UState.subst universes) in
   let make_body =
     if poly || now then
       let make_body t (c, eff) =
@@ -436,7 +436,7 @@ let return_proof ?(allow_partial=false) () =
     | Proof.HasUnresolvedEvar->
         error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd = Evd.nf_constraints evd in
+  let evd = Evd.minimize_universes evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
diff --git a/stm/stm.ml b/stm/stm.ml
index d878bbb30..b3da97c6e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2482,7 +2482,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                   match keep with
                   | VtDrop -> None
                   | VtKeepAsAxiom ->
-                      let ctx = Evd.empty_evar_universe_context in
+                      let ctx = UState.empty in
                       let fp = Future.from_val ([],ctx) in
                       qed.fproof <- Some (fp, ref false); None
                   | VtKeep ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 45926551b..477de6452 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -214,7 +214,7 @@ let build_sym_scheme env ind =
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
        [|cstr (nrealargs+1)|]))))
-  in c, Evd.evar_universe_context_of ctx
+  in c, UState.of_context_set ctx
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
@@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind =
 	       mkRel 1|])),
 	       mkRel 1 (* varH *),
 	       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
-  in (c, Evd.evar_universe_context_of ctx), eff
+  in (c, UState.of_context_set ctx), eff
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
@@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, Evd.evar_universe_context_of ctx),
+  in (c, UState.of_context_set ctx),
       Safe_typing.concat_private eff' eff
 
 (**********************************************************************)
@@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 	  (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda varHC applied_PC'
 	(mkVar varHC))|])))))
-  in c, Evd.evar_universe_context_of ctx
+  in c, UState.of_context_set ctx
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
 	   lift (nrealargs+3) applied_PC,
 	   mkRel 1)|]),
     [|mkVar varHC|]))))))
-  in c, Evd.evar_universe_context_of ctx
+  in c, UState.of_context_set ctx
 
 (**********************************************************************)
 (* This function "repairs" the non-dependent r2l forward rewriting    *)
@@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind =
        [|mkApp (refl,
           [|mkVar varB;
 	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
-  in c, Evd.evar_universe_context_of ctx
+  in c, UState.of_context_set ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index b960a845c..62ead57f3 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -122,8 +122,8 @@ let compute_name internal id =
 let define internal id c p univs =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
-  let ctx = Evd.normalize_evar_universe_context univs in
-  let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in
+  let ctx = UState.minimize univs in
+  let c = Universes.subst_opt_univs_constr (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/tactics/leminv.ml b/tactics/leminv.ml
index 655283c20..a4cdc1592 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   end in
   let avoid = ref Id.Set.empty in
   let _,_,_,_,sigma = Proof.proof pf in
-  let sigma = Evd.nf_constraints sigma in
+  let sigma = Evd.minimize_universes sigma in
   let rec fill_holes c =
     match EConstr.kind sigma c with
     | Evar (e,args) ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9b7b88b51..2879feba7 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -323,7 +323,7 @@ let build_beq_scheme mode kn =
 	  raise NoDecidabilityCoInductive;
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
-       Evd.make_evar_universe_context (Global.env ()) None),
+       UState.make (Global.universes ())),
       !eff
 
 let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -671,7 +671,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
+  let ctx = UState.make (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
@@ -795,7 +795,7 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
+  let ctx = UState.make (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
@@ -965,7 +965,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = Evd.make_evar_universe_context (Global.env ()) None in
+  let ctx = UState.make (Global.universes ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 1712634da..6a590758f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -160,7 +160,7 @@ let do_assumptions kind nl l =
   in
   let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
   (* The universe constraints come from the whole telescope. *)
-  let sigma = Evd.nf_constraints sigma in
+  let sigma = Evd.minimize_universes sigma in
   let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 01dbe0a0d..b18a60a1f 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt =
       evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
   in
   (* universe minimization *)
-  let evd = Evd.nf_constraints evd in
+  let evd = Evd.minimize_universes evd in
   (* Substitute evars and universes, and add parameters.
      Note: in program mode some evars may remain. *)
   let ctx = List.map (EConstr.to_rel_decl evd) ctx in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 41c44b126..27587416b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -381,7 +381,7 @@ let do_mutual_induction_scheme lnamedepindsort =
 	 | None ->
 	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
 	    let u, ctx = Universes.fresh_instance_from ctx None in
-	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in
+            let evd = Evd.from_ctx (UState.of_context_set ctx) in
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
        in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6447fc350..4f16e1cf6 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -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)
-    (Evd.evar_universe_context_subst prg.prg_ctx) in
+    (UState.subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
   let typ = nf typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5779c07ab..5eae4fd7f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -72,7 +72,7 @@ let show_top_evars () =
 let show_universes () =
   let pfts = Proof_global.give_me_the_proof () in
   let gls,_,_,_,sigma = Proof.proof pfts in
-  let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
+  let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
   Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
   str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx