diff options
| -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 |