From 66973ce17e32a3c692a5b0032f38300ec8cc36d3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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
---
 engine/uState.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 67479351a..e57afd743 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -585,7 +585,7 @@ let refresh_undefined_univ_variables uctx =
                uctx_initial_universes = initial } in
     uctx', subst
 
-let normalize uctx = 
+let minimize uctx =
   let ((vars',algs'), us') = 
     Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
 				    uctx.uctx_univ_algebraic
@@ -613,3 +613,6 @@ let update_sigma_env uctx env =
                          uctx_universes = univs }
   in
   merge true univ_rigid eunivs eunivs.uctx_local
+
+(** Deprecated *)
+let normalize = minimize
-- 
cgit v1.2.3