{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

1 files changed, 11 insertions, 0 deletions

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