From ddcb5ebd626336382199d796ad2c850ac63073df Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 9 Oct 2019 15:29:39 +0200
Subject: universes_of_private: return set instead of list of sets

---
 engine/uState.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3