Deprecate UState aliases in Evd.

5 files changed, 57 insertions, 45 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index e7d542d12..47fa48d4f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -253,21 +253,8 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-type evar_universe_context = UState.t
-
-type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let add_universe_constraints_context = UState.add_universe_constraints
-let constrain_variables = UState.constrain_variables 
-let evar_universe_context_of_binders = UState.of_binders
+type 'a in_evar_universe_context = 'a * UState.t
 
 (*******************************************************************)
 (* Metamaps *)
@@ -427,7 +414,7 @@ type evar_map = {
   undf_evars : evar_info EvMap.t;
   evar_names : EvNames.t;
   (** Universes *)
-  universes  : evar_universe_context;
+  universes  : UState.t;
   (** Conversion problems *)
   conv_pbs   : evar_constraint list;
   last_mods  : Evar.Set.t;
@@ -558,10 +545,10 @@ let existential_type d (n, args) =
   instantiate_evar_array info info.evar_concl args
 
 let add_constraints d c =
-  { d with universes = add_constraints_context d.universes c }
+  { d with universes = UState.add_constraints d.universes c }
 
 let add_universe_constraints d c = 
-  { d with universes = add_universe_constraints_context d.universes c }
+  { d with universes = UState.add_universe_constraints d.universes c }
 
 (*** /Lifting... ***)
 
@@ -586,7 +573,7 @@ let create_evar_defs sigma = { sigma with
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
-  universes  = empty_evar_universe_context;
+  universes  = UState.empty;
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
@@ -609,14 +596,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
   let universes = 
     if not with_univs then evd.universes
-    else union_evar_universe_context evd.universes d.universes
+    else UState.union evd.universes d.universes
   in
   { evd with
     metas = d.metas;
     last_mods; conv_pbs; universes }
 
 let merge_universe_context evd uctx' =
-  { evd with universes = union_evar_universe_context evd.universes uctx' }
+  { evd with universes = UState.union evd.universes uctx' }
 
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
@@ -798,16 +785,6 @@ let make_flexible_variable evd ~algebraic u =
   { evd with universes =
       UState.make_flexible_variable evd.universes ~algebraic u }
 
-let make_evar_universe_context e l =
-  let uctx = UState.make (Environ.universes e) in
-  match l with
-  | None -> uctx
-  | Some us ->
-      List.fold_left
-        (fun uctx { CAst.loc; v = id } ->
-        fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
-        uctx us
-
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -910,10 +887,6 @@ let check_eq evd s s' =
 let check_leq evd s s' =
   UGraph.check_leq (UState.ugraph evd.universes) s s'
 
-let normalize_evar_universe_context_variables = UState.normalize_variables
-
-let abstract_undefined_variables = UState.abstract_undefined_variables
-
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
@@ -922,16 +895,14 @@ let refresh_undefined_universes evd =
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let normalize_evar_universe_context = UState.normalize
-
-let nf_univ_variables evd = 
-  let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
+let nf_univ_variables evd =
+  let subst, uctx' = UState.normalize_variables evd.universes in
   let evd' = {evd with universes = uctx'} in
     evd', subst
 
 let nf_constraints evd =
-  let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
-  let uctx' = normalize_evar_universe_context uctx' in
+  let subst, uctx' = UState.normalize_variables evd.universes in
+  let uctx' = UState.normalize uctx' in
     {evd with universes = uctx'}
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
@@ -1076,7 +1047,7 @@ let clear_metas evd = {evd with metas = Metamap.empty}
 let meta_merge ?(with_univs = true) evd1 evd2 =
   let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in
   let universes =
-    if with_univs then union_evar_universe_context evd2.universes evd1.universes
+    if with_univs then UState.union evd2.universes evd1.universes
     else evd2.universes
   in
   {evd2 with universes; metas; }
@@ -1176,3 +1147,24 @@ module Monad =
 (* Failure explanation *)
 
 type unsolvability_explanation = SeveralInstancesFound of int
+
+(** Deprecated *)
+type evar_universe_context = UState.t
+let empty_evar_universe_context = UState.empty
+let union_evar_universe_context = UState.union
+let evar_universe_context_set = UState.context_set
+let evar_universe_context_constraints = UState.constraints
+let evar_context_universe_context = UState.context
+let evar_universe_context_of = UState.of_context_set
+let evar_universe_context_subst = UState.subst
+let add_constraints_context = UState.add_constraints
+let constrain_variables = UState.constrain_variables
+let evar_universe_context_of_binders = UState.of_binders
+let make_evar_universe_context e l =
+  let g = Environ.universes e in
+  match l with
+  | None -> UState.make g
+  | 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
diff --git a/engine/evd.mli b/engine/evd.mli
index 55b8e3a83..25dc8c993 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,22 +493,31 @@ val univ_flexible_alg : rigid
 type 'a in_evar_universe_context = 'a * UState.t
 
 val evar_universe_context_set : UState.t -> Univ.ContextSet.t
+[@@ocaml.deprecated "Alias of UState.context_set"]
 val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
+[@@ocaml.deprecated "Alias of UState.constraints"]
 val evar_context_universe_context : UState.t -> Univ.UContext.t
 [@@ocaml.deprecated "alias of UState.context"]
 
 val evar_universe_context_of : Univ.ContextSet.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.of_context_set"]
 val empty_evar_universe_context : UState.t
+[@@ocaml.deprecated "Alias of UState.empty"]
 val union_evar_universe_context : UState.t -> UState.t ->
   UState.t
+[@@ocaml.deprecated "Alias of UState.union"]
 val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst
+[@@ocaml.deprecated "Alias of UState.subst"]
 val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.constrain_variables"]
 
 
 val evar_universe_context_of_binders :
   Universes.universe_binders -> UState.t
+[@@ocaml.deprecated "Alias of UState.of_binders"]
 
 val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
+[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
 val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t
@@ -516,13 +525,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 val universe_binders : evar_map -> Universes.universe_binders
 val add_constraints_context : UState.t ->
   Univ.Constraint.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.add_constraints"]
 
 
 val normalize_evar_universe_context_variables : UState.t -> 
   Univ.universe_subst in_evar_universe_context
+[@@ocaml.deprecated "Alias of UState.normalize_variables"]
 
-val normalize_evar_universe_context : UState.t -> 
-  UState.t
+val normalize_evar_universe_context : UState.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.normalize"]
 
 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
@@ -581,6 +592,7 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : UState.t -> UState.t
+[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
 
 val fix_undefined_variables : evar_map -> evar_map
 
diff --git a/engine/termops.ml b/engine/termops.ml
index c615155d1..35258762a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont
 
 let pr_evar_universe_context ctx =
   let open UState in
-  let open Evd in
   let prl = pr_uctx_level ctx in
   if UState.is_empty ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
diff --git a/engine/uState.ml b/engine/uState.ml
index 00825208b..67479351a 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
diff --git a/engine/uState.mli b/engine/uState.mli
index 68fe350c0..ef7cee32e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,6 +26,8 @@ val empty : t
 
 val make : UGraph.t -> t
 
+val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+
 val is_empty : t -> bool
 
 val union : t -> t -> t