diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 16:00:06 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 16:00:41 +0200 |
commit | b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (patch) | |
tree | 1505041402d00c52669f9e430d144c97eae490ff /kernel | |
parent | dbdef043ea143f871a3710bae36dfc45fd815835 (diff) |
Univs: fix bug #3807
Add a flag to disallow minimization to set
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/univ.ml | 3 | ||||
-rw-r--r-- | kernel/univ.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 34eb283d7..c0bd3bacd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1797,6 +1797,9 @@ struct let empty = (LSet.empty, Constraint.empty) let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst + let equal (univs, cst as x) (univs', cst' as y) = + x == y || (LSet.equal univs univs' && Constraint.equal cst cst') + let of_set s = (s, Constraint.empty) let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) diff --git a/kernel/univ.mli b/kernel/univ.mli index 4cc8a2528..cbaf7e546 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -360,6 +360,7 @@ sig val of_instance : Instance.t -> t val of_set : universe_set -> t + val equal : t -> t -> bool val union : t -> t -> t val append : t -> t -> t |