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/eConstr.ml | |
| parent | 98c0c64749b6656df2a6522a3277ca2b96ae58ba (diff) | |
| parent | ea87cce3f81e9b73047c1695ea716162aeb09ede (diff) | |
Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index ea098902a2..d303038c5d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,12 +645,25 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr sigma c = +let universes_of_constr env sigma c = let open Univ in + let open Declarations in let rec aux s c = match kind sigma c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma 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 (EInstance.kind sigma u)) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s |