diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-22 16:09:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-26 13:33:51 +0200 |
| commit | 05dff3bdaaf474e67b0878bc2dd0952427ce277e (patch) | |
| tree | 61aca8104fd4e3729d06c392f3fa9bd9b6db06bd /engine/univops.ml | |
| parent | df35025b2be4a0dc9aadecc0e3110a21012683cf (diff) | |
universes_of_constr don't include universes of monomorphic constants
Apparently it was not useful. I don't remember what I was thinking
when I added it.
Diffstat (limited to 'engine/univops.ml')
| -rw-r--r-- | engine/univops.ml | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/engine/univops.ml b/engine/univops.ml index 3fd518490..7f9672f82 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -11,24 +11,13 @@ open Univ open Constr -let universes_of_constr env c = - let open Declarations in - let rec aux s c = +let universes_of_constr c = + let rec aux s c = match kind c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s |