Rename some universe minimizing "normalize" functions to "minimize"

UState normalize -> minimize, Evd nf_constraints -> minimize_universes

5 files changed, 18 insertions, 8 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 7674cf67a..6b3ce048f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -89,15 +89,15 @@ let nf_evars_universes evm =
     (Evd.universe_subst evm)
     
 let nf_evars_and_universes evm =
-  let evm = Evd.nf_constraints evm in
+  let evm = Evd.minimize_universes evm in
     evm, nf_evars_universes evm
 
 let e_nf_evars_and_universes evdref =
-  evdref := Evd.nf_constraints !evdref;
+  evdref := Evd.minimize_universes !evdref;
   nf_evars_universes !evdref, Evd.universe_subst !evdref
 
 let nf_evar_map_universes evm =
-  let evm = Evd.nf_constraints evm in
+  let evm = Evd.minimize_universes evm in
   let subst = Evd.universe_subst evm in
     if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
diff --git a/engine/evd.ml b/engine/evd.ml
index 47fa48d4f..185cab101 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -900,9 +900,9 @@ let nf_univ_variables evd =
   let evd' = {evd with universes = uctx'} in
     evd', subst
 
-let nf_constraints evd =
+let minimize_universes evd =
   let subst, uctx' = UState.normalize_variables evd.universes in
-  let uctx' = UState.normalize uctx' in
+  let uctx' = UState.minimize uctx' in
     {evd with universes = uctx'}
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
@@ -1167,4 +1167,5 @@ let make_evar_universe_context e l =
   | Some l -> UState.make_with_initial_binders g l
 let normalize_evar_universe_context_variables = UState.normalize_variables
 let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.normalize
+let normalize_evar_universe_context = UState.minimize
+let nf_constraints = minimize_universes
diff --git a/engine/evd.mli b/engine/evd.mli
index 25dc8c993..7957eaa01 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -533,7 +533,7 @@ val normalize_evar_universe_context_variables : UState.t ->
 [@@ocaml.deprecated "Alias of UState.normalize_variables"]
 
 val normalize_evar_universe_context : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.normalize"]
+[@@ocaml.deprecated "Alias of UState.minimize"]
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
 val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -598,7 +598,10 @@ val fix_undefined_variables : evar_map -> evar_map
 
 val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
 
+(** Universe minimization *)
+val minimize_universes : evar_map -> evar_map
 val nf_constraints : evar_map -> evar_map
+[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
 
 val update_sigma_env : evar_map -> env -> evar_map
 
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
diff --git a/engine/uState.mli b/engine/uState.mli
index ef7cee32e..9a2bc706b 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -133,7 +133,10 @@ val fix_undefined_variables : t -> t
 
 val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
+(** Universe minimization *)
+val minimize : t -> t
 val normalize : t -> t
+[@@ocaml.deprecated "Alias of UState.minimize"]
 
 type universe_decl =
   (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl