Merge PR #6893: Cleanup UState API usage

3 files changed, 9 insertions, 9 deletions

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) ->