diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d66ae911d3..dd43e17be5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1882,8 +1882,9 @@ struct let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) - let union (univs, cst) (univs', cst') = - LSet.union univs univs', Constraint.union cst cst' + let union (univs, cst as x) (univs', cst' as y) = + if x == y then x + else LSet.union univs univs', Constraint.union cst cst' let append (univs, cst) (univs', cst') = let univs = LSet.fold LSet.add univs univs' in |