diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 7835a807ba..38a428d9a1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -382,6 +382,18 @@ let add_universes_set strict ctx g = let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env +let push_subgraph (levels,csts) env = + let add_subgraph g = + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = UGraph.merge_constraints csts newg in + (if not (Univ.Constraint.is_empty csts) then + let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in + (if not (UGraph.check_constraints restricted g) then + CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints."))); + newg + in + map_universes add_subgraph env + let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = c } } |