Merge PR #10863: Minor side effect universe cleanups

Ack-by: JasonGross
Reviewed-by: ppedrot

4 files changed, 8 insertions, 9 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
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fc55720583..98465c070b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -320,10 +320,10 @@ let concat_private = SideEffects.concat
 let universes_of_private eff =
   let fold acc eff =
     match eff.seff_body.const_universes with
-    | Monomorphic ctx -> ctx :: acc
+    | Monomorphic ctx -> Univ.ContextSet.union ctx acc
     | Polymorphic _ -> acc
   in
-  List.fold_left fold [] (side_effects_of_private_constants eff)
+  List.fold_left fold Univ.ContextSet.empty (side_effects_of_private_constants eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b55293f1c..1ce790ebbb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -59,7 +59,7 @@ val inline_private_constants :
 val push_private_constants : Environ.env -> private_constants -> Environ.env
 (** Push the constants in the environment if not already there. *)
 
-val universes_of_private : private_constants -> Univ.ContextSet.t list
+val universes_of_private : private_constants -> Univ.ContextSet.t
 
 val is_curmod_library : safe_environment -> bool
 
diff --git a/test-suite/bugs/closed/bug_6323.v b/test-suite/bugs/closed/bug_6323.v
index fdc33befc6..24feb7155c 100644
--- a/test-suite/bugs/closed/bug_6323.v
+++ b/test-suite/bugs/closed/bug_6323.v
@@ -6,4 +6,5 @@ Goal True.
       simple refine (let id' : { x : X' | True } -> X' := _ in _);
       [ abstract refine (@proj1_sig _ _) | ]
     ].
-Abort.
+  exact I.
+Defined.