aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml44
1 files changed, 22 insertions, 22 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index cd0b52eca..3f4bfe7af 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -283,8 +283,8 @@ type evar_universe_context =
(** The subset of unification variables that
can be instantiated with algebraic universes as they appear in types
and universe instances only. *)
- uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
- uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+ uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+ uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
}
let empty_evar_universe_context =
@@ -292,8 +292,8 @@ let empty_evar_universe_context =
uctx_local = Univ.ContextSet.empty;
uctx_univ_variables = Univ.LMap.empty;
uctx_univ_algebraic = Univ.LSet.empty;
- uctx_universes = Univ.initial_universes;
- uctx_initial_universes = Univ.initial_universes }
+ uctx_universes = UGraph.initial_universes;
+ uctx_initial_universes = UGraph.initial_universes }
let evar_universe_context_from e =
let u = universes e in
@@ -314,7 +314,7 @@ let union_evar_universe_context ctx ctx' =
(Univ.ContextSet.levels ctx.uctx_local) in
let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
let declarenew g =
- Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+ Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
in
let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
@@ -328,7 +328,7 @@ let union_evar_universe_context ctx ctx' =
if local == ctx.uctx_local then ctx.uctx_universes
else
let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
- Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+ UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
(* let union_evar_universe_context = *)
@@ -374,7 +374,7 @@ let process_universe_constraints univs vars alg cstrs =
| Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
in
if d == Universes.ULe then
- if Univ.check_leq univs l r then
+ if UGraph.check_leq univs l r then
(** Keep Prop/Set <= var around if var might be instantiated by prop or set
later. *)
if Univ.Universe.is_level l then
@@ -413,7 +413,7 @@ let process_universe_constraints univs vars alg cstrs =
instantiate_variable l' r vars
else if rloc then
instantiate_variable r' l vars
- else if not (Univ.check_eq univs l r) then
+ else if not (UGraph.check_eq univs l r) then
(* Two rigid/global levels, none of them being local,
one of them being Prop/Set, disallow *)
if Univ.Level.is_small l' || Univ.Level.is_small r' then
@@ -433,7 +433,7 @@ let process_universe_constraints univs vars alg cstrs =
Univ.enforce_leq inst lu local
else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
| _, _ (* One of the two is algebraic or global *) ->
- if Univ.check_eq univs l r then local
+ if UGraph.check_eq univs l r then local
else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
in
let local =
@@ -459,7 +459,7 @@ let add_constraints_context ctx cstrs =
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
- uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+ uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -473,7 +473,7 @@ let add_universe_constraints_context ctx cstrs =
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
- uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+ uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
(* let add_universe_constraints_context = *)
@@ -1012,13 +1012,13 @@ let merge_uctx sideff rigid uctx ctx' =
in
let declare g =
LSet.fold (fun u g ->
- try Univ.add_universe u false g
- with Univ.AlreadyDeclared when sideff -> g)
+ try UGraph.add_universe u false g
+ with UGraph.AlreadyDeclared when sideff -> g)
levels g
in
let initial = declare uctx.uctx_initial_universes in
let univs = declare uctx.uctx_universes in
- let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+ let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
{ uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
let merge_context_set rigid evd ctx' =
@@ -1079,11 +1079,11 @@ let uctx_new_univ_variable rigid name predicative
| None -> uctx.uctx_names
in
let initial =
- Univ.add_universe u false uctx.uctx_initial_universes
+ UGraph.add_universe u false uctx.uctx_initial_universes
in
let uctx' =
{uctx' with uctx_names = names; uctx_local = ctx';
- uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+ uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
uctx_initial_universes = initial}
in uctx', u
@@ -1102,10 +1102,10 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
let add_global_univ d u =
let uctx = d.universes in
let initial =
- Univ.add_universe u true uctx.uctx_initial_universes
+ UGraph.add_universe u true uctx.uctx_initial_universes
in
let univs =
- Univ.add_universe u true uctx.uctx_universes
+ UGraph.add_universe u true uctx.uctx_universes
in
{ d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
uctx_initial_universes = initial;
@@ -1245,10 +1245,10 @@ let set_leq_sort env evd s1 s2 =
else evd
let check_eq evd s s' =
- Univ.check_eq evd.universes.uctx_universes s s'
+ UGraph.check_eq evd.universes.uctx_universes s s'
let check_leq evd s s' =
- Univ.check_leq evd.universes.uctx_universes s s'
+ UGraph.check_leq evd.universes.uctx_universes s s'
let subst_univs_context_with_def def usubst (ctx, cst) =
(Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
@@ -1301,10 +1301,10 @@ let refresh_undefined_univ_variables uctx =
(Option.map (Univ.subst_univs_level_universe subst) v) acc)
uctx.uctx_univ_variables Univ.LMap.empty
in
- let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+ let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
(Univ.ContextSet.levels ctx') g in
let initial = declare uctx.uctx_initial_universes in
- let univs = declare Univ.initial_universes in
+ let univs = declare UGraph.initial_universes in
let uctx' = {uctx_names = uctx.uctx_names;
uctx_local = ctx';
uctx_univ_variables = vars; uctx_univ_algebraic = alg;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 21:13:49 +0000