universes_of_private: return set instead of list of sets

1 files changed, 3 insertions, 5 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index efced52990..ba17cdde93 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -539,11 +539,9 @@ let merge_seff uctx ctx' =
               uctx_initial_universes = initial }
 
 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 (fst uctx) u in
-      merge_seff u uctx)
-    u uctxs
+  let uctx = Safe_typing.universes_of_private eff in
+  let u = demote_seff_univs (fst uctx) u in
+  merge_seff u uctx
 
 let update_sigma_env uctx env =
   let univs = UGraph.make_sprop_cumulative (Environ.universes env) in