diff options
| -rw-r--r-- | kernel/univ.ml | 5 | ||||
| -rw-r--r-- | kernel/univ.mli | 5 |
2 files changed, 10 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d3201bcb9..942c90aa2 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1876,6 +1876,11 @@ struct let union (univs, cst) (univs', cst') = LSet.union univs univs', Constraint.union cst cst' + let append (univs, cst) (univs', cst') = + let univs = LSet.fold LSet.add univs univs' in + let cst = Constraint.fold Constraint.add cst cst' in + (univs, cst) + let diff (univs, cst) (univs', cst') = LSet.diff univs univs', Constraint.diff cst cst' diff --git a/kernel/univ.mli b/kernel/univ.mli index 3779c055d..c9b7547f2 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -339,6 +339,11 @@ sig val of_set : universe_set -> t val union : t -> t -> t + + val append : t -> t -> t + (** Variant of {!union} which is more efficient when the left argument is + much smaller than the right one. *) + val diff : t -> t -> t val add_universe : universe_level -> t -> t val add_constraints : constraints -> t -> t |