From 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 20:07:33 +0100
Subject: Optimizing the universes_of_constr_function.

Instead of relying on a costly set union, we take advantage of the fact
that instances are small compared to the set of universes.
---
 library/universes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/universes.ml b/library/universes.ml
index 7972c478ad..3bebdafc78 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -959,10 +959,10 @@ let universes_of_constr c =
   let rec aux s c = 
     match kind_of_term c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.union (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
       let u = univ_of_sort u in
-	LSet.union (Universe.levels u) s
+      LSet.fold LSet.add (Universe.levels u) s
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
-- 
cgit v1.2.3