{Univops->UState}.restrict_universe_context

Thus the adhoc univops can be removed at the end of the deprecation period.

Should we keep exposing restrict_universe_context or make people go
through restrict?

restrict_universe_context is used directly only by newring, where it's
a choice between

    let univs = UState.restrict_universe_context univs vars in

and

    let univs = UState.(context_set (restrict (of_context_set univs) vars)) in

6 files changed, 29 insertions, 20 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
 UnivProblem
 UnivMinim
 Universes
-Univops
 UState
+Univops
 Nameops
 Evar_kinds
 Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..aa7ec63a6f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl =
       (Univ.ContextSet.constraints uctx.uctx_local);
   ctx
 
+let restrict_universe_context (univs, csts) keep =
+  let open Univ in
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
+  (LSet.inter univs keep, csts)
+
 let restrict ctx vars =
   let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 let demote_seff_univs entry uctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..8053a7bf83 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
     primitives when needed. *)
 
 open Names
+open Univ
 
 exception UniversesDiffer
 
@@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+   [ctx] extended by local named universes and side effect universes
+   (from [demote_seff_univs]). Transitive constraints between retained
+   universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
 val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
diff --git a/engine/univops.ml b/engine/univops.ml
index c933641865..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,18 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Univ
-
 let universes_of_constr = Vars.universes_of_constr
 
-let restrict_universe_context (univs, csts) keep =
-  let removed = LSet.diff univs keep in
-  if LSet.is_empty removed then univs, csts
-  else
-  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
-  let g = UGraph.empty_universes in
-  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
-  let g = UGraph.merge_constraints csts g in
-  let allkept = LSet.diff allunivs removed in
-  let csts = UGraph.constraints_for ~kept:allkept g in
-  (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 0ed06bb204..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,8 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
-   the universes in [keep]. The constraints [csts] are adjusted so
-   that transitive constraints between remaining universes (those in
-   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index cf959bd11f..9585826109 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *)
 let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
-  let univs = Univops.restrict_universe_context univs vars in
+  let univs = UState.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),