diff options
| -rw-r--r-- | kernel/univ.ml | 12 | ||||
| -rw-r--r-- | kernel/univ.mli | 5 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 |
3 files changed, 13 insertions, 6 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 86aebbce9..d3201bcb9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1879,11 +1879,17 @@ struct let diff (univs, cst) (univs', cst') = LSet.diff univs univs', Constraint.diff cst cst' - let add_constraints (univs, cst) cst' = + let add_universe u (univs, cst) = + LSet.add u univs, cst + + let add_constraints cst' (univs, cst) = univs, Constraint.union cst cst' - let add_universes univs ctx = - union (of_instance univs) ctx + let add_instance inst (univs, cst) = + let v = Instance.to_array inst in + let fold accu u = LSet.add u accu in + let univs = Array.fold_left fold univs v in + (univs, cst) let to_context (ctx, cst) = (Instance.of_array (Array.of_list (LSet.elements ctx)), cst) diff --git a/kernel/univ.mli b/kernel/univ.mli index 655f87bb5..3779c055d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -340,8 +340,9 @@ sig val union : t -> t -> t val diff : t -> t -> t - val add_constraints : t -> constraints -> t - val add_universes : Instance.t -> t -> t + val add_universe : universe_level -> t -> t + val add_constraints : constraints -> t -> t + val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) val to_context : t -> universe_context diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c60fb2958..c5657cc52 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -989,7 +989,7 @@ let with_context_set rigid d (a, ctx) = let uctx_new_univ_variable rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in - let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in + let ctx' = Univ.ContextSet.add_universe u ctx in let uctx' = match rigid with | UnivRigid -> uctx |