From 5d926b0279f70250db1ee54edcdb4e855ac96f0f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Mar 2018 14:58:00 +0100
Subject: Deprecate UState aliases in Evd.

---
 engine/uState.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'engine/uState.ml')

diff --git a/engine/uState.ml b/engine/uState.ml
index 00825208b3..67479351ab 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name
                 uctx_initial_universes = initial}
   in uctx', u
 
+let make_with_initial_binders e us =
+  let uctx = make e in
+  List.fold_left
+    (fun uctx { CAst.loc; v = id } ->
+       fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
+    uctx us
+
 let add_global_univ uctx u =
   let initial =
     UGraph.add_universe u true uctx.uctx_initial_universes
-- 
cgit v1.2.3


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
---
 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 67479351ab..e57afd743a 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