diff options
| author | Pierre-Marie Pédrot | 2016-02-03 20:07:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-03 20:24:06 +0100 |
| commit | 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 (patch) | |
| tree | ca8aca465c51893aef9f8237338ef4e4aca472e5 | |
| parent | 62c141be71dd3c542824c19429eac0fdd686c9cb (diff) | |
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.
| -rw-r--r-- | library/universes.ml | 4 |
1 files 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 |