Merge PR #10913: re-expose UState.demote_seff_univs

Ack-by: gares
Reviewed-by: ppedrot

2 files changed, 7 insertions, 2 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index af714f6282..efced52990 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -520,7 +520,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
 
-let demote_seff_univs (univs,_) uctx =
+let demote_seff_univs univs uctx =
   let seff = LSet.union uctx.uctx_seff_univs univs in
   { uctx with uctx_seff_univs = seff }
 
@@ -541,7 +541,7 @@ let merge_seff uctx ctx' =
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
   List.fold_left (fun u uctx ->
-      let u = demote_seff_univs uctx u in
+      let u = demote_seff_univs (fst uctx) u in
       merge_seff u uctx)
     u uctxs
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 7cb2f49780..23ef84c55d 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -112,6 +112,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_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
+   emit_side_effects instead. *)
+
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t