From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/environ.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 1cc07c0ab..09fe64d77 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -188,10 +188,10 @@ let map_universes f env = let add_constraints c env = if Univ.Constraint.is_empty c then env - else map_universes (Univ.merge_constraints c) env + else map_universes (UGraph.merge_constraints c) env let check_constraints c env = - Univ.check_constraints c env.env_stratification.env_universes + UGraph.check_constraints c env.env_stratification.env_universes let push_constraints_to_env (_,univs) env = add_constraints univs env @@ -199,19 +199,19 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in - Univ.merge_constraints (Univ.UContext.constraints ctx) g + UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = let g = Univ.LSet.fold - (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g - in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env -- cgit v1.2.3