Merge PR #6893: Cleanup UState API usage

6 files changed, 9 insertions, 9 deletions

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