From dbc820f0df53218e730eba34b44a3b1901f13b9e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc088..482571ea8 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