From eec72af81a84f7b56b04027693684eebe139a607 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Aug 2014 13:18:25 +0200
Subject: Tentative performance fix for Evd.merge_uctx.

The levels added by the context are in general much fewer than the size of the
evarmap, so it is better to add them to the latter rather than doing it the
other way around.
---
 pretyping/evd.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cd02d7228a..c60fb29586 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -960,8 +960,11 @@ let merge_uctx rigid uctx ctx' =
     | UnivRigid -> uctx
     | UnivFlexible b ->
       let levels = Univ.ContextSet.levels ctx' in
-      let uvars' = Univ.LMap.bind (fun _ -> None) levels in
-      let uvars' = Univ.LMap.fold Univ.LMap.add uctx.uctx_univ_variables uvars' in
+      let fold u accu =
+        if Univ.LMap.mem u accu then accu
+        else Univ.LMap.add u None accu
+      in
+      let uvars' = Univ.LSet.fold fold levels uctx.uctx_univ_variables in
 	if b then
 	  { uctx with uctx_univ_variables = uvars';
 	  uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic levels }
-- 
cgit v1.2.3