From dbc820f0df53218e730eba34b44a3b1901f13b9e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Mar 2018 15:50:32 +0100
Subject: Deprecate mixing univ minimization and evm normalization functions.

Normalization sounds like it should be semantically noop.
---
 tactics/elimschemes.ml | 4 ++--
 tactics/tactics.ml     | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 6bd4866c61..70f73df5c1 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
 	mib.mind_nparams in
     let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
     let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
-    let sigma, nf = Evarutil.nf_evars_and_universes sigma in
-      (nf c', Evd.evar_universe_context sigma), eff
+    let sigma = Evd.minimize_universes sigma in
+    (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
   else
     let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc0885..482571ea87 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4929,9 +4929,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
 
   let evd, ctx, concl =
     (* FIXME: should be done only if the tactic succeeds *)
-    let evd, nf = nf_evars_and_universes !evdref in
+    let evd = Evd.minimize_universes !evdref in
     let ctx = Evd.universe_context_set evd in
-      evd, ctx, nf concl
+      evd, ctx, Evarutil.nf_evars_universes evd concl
   in
   let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
-- 
cgit v1.2.3