diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index 7d1908d1f5..f1c9c85a20 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -645,7 +645,7 @@ let universes_of_constr c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> LSet.union (Instance.levels u) s - | Sort u -> + | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in LSet.union (Universe.levels u) s | _ -> fold_constr aux s c |