diff options
| author | Matthieu Sozeau | 2014-12-14 18:54:24 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-12-14 19:06:14 +0100 |
| commit | 2db658105f8ed20ca2153271b339c777b79da406 (patch) | |
| tree | 9aedc88d0c0338c98b9f68300f16f52f2f0aa44b /kernel | |
| parent | e117099919cb0a474cad4fe2a6d15165b2520760 (diff) | |
Fix merging of name maps in union of universe contexts.
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 |