diff options
| author | Gaëtan Gilbert | 2019-10-09 15:29:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-19 11:26:25 +0200 |
| commit | ddcb5ebd626336382199d796ad2c850ac63073df (patch) | |
| tree | 76a16382bacfbd638fd5984ee5fff0cfb40dfa76 | |
| parent | c5f2b14020ea1fb2b11321f1daa00abe8dec3477 (diff) | |
universes_of_private: return set instead of list of sets
| -rw-r--r-- | engine/uState.ml | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
3 files changed, 6 insertions, 8 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 |