From 66973ce17e32a3c692a5b0032f38300ec8cc36d3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Mar 2018 15:10:39 +0100
Subject: Rename some universe minimizing  "normalize" functions to "minimize"

UState normalize -> minimize, Evd nf_constraints -> minimize_universes
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6e38b46413..e0368153e5 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
-- 
cgit v1.2.3