From 2db658105f8ed20ca2153271b339c777b79da406 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 14 Dec 2014 18:54:24 +0100
Subject: Fix merging of name maps in union of universe contexts.

---
 kernel/univ.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3