[univ] API to demote global universes

2 files changed, 13 insertions, 0 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index ff85f09efa..e4e1d4f1d4 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -527,6 +527,14 @@ let demote_seff_univs univs uctx =
   let seff = LSet.union uctx.uctx_seff_univs univs in
   { uctx with uctx_seff_univs = seff }
 
+let demote_global_univs env uctx =
+  let env_ugraph = Environ.universes env in
+  let global_univs = UGraph.domain env_ugraph in
+  let global_constraints, _ = UGraph.constraints_of_universes env_ugraph in
+  let promoted_uctx =
+    ContextSet.(of_set global_univs |> add_constraints global_constraints) in
+  { uctx with uctx_local = ContextSet.diff uctx.uctx_local promoted_uctx }
+
 let merge_seff uctx ctx' =
   let levels = ContextSet.levels ctx' in
   let declare g =
diff --git a/engine/uState.mli b/engine/uState.mli
index cd1c9a174e..6707826aae 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -110,6 +110,11 @@ val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
+val demote_global_univs : Environ.env -> t -> t
+(** Removes from the uctx_local part of the UState the universes and constraints
+    that are present in the universe graph in the input env (supposedly the
+    global ones *)
+
 val demote_seff_univs : Univ.LSet.t -> t -> t
 (** Mark the universes as not local any more, because they have been
    globally declared by some side effect. You should be using