diff options
| author | Maxime Dénès | 2017-12-11 11:32:20 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 11:32:20 +0100 |
| commit | 340e90e366e002e475fb0e6c4718b8614c95f366 (patch) | |
| tree | 0313a27a044e39ae6a1ba9f4dedad151fa8ed752 /engine/univops.ml | |
| parent | 98c0c64749b6656df2a6522a3277ca2b96ae58ba (diff) | |
| parent | ea87cce3f81e9b73047c1695ea716162aeb09ede (diff) | |
Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.
Diffstat (limited to 'engine/univops.ml')
| -rw-r--r-- | engine/univops.ml | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/engine/univops.ml b/engine/univops.ml index 9a9ae12cab..df25d87252 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -9,12 +9,25 @@ open Univ open Constr -let universes_of_constr c = +let universes_of_constr env c = + let open Declarations in let rec aux s c = match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> + | 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 | _ -> Constr.fold aux s c |