diff options
| author | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 16:31:32 +0100 |
| commit | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (patch) | |
| tree | 754bd11791e63df535dff44a58e126ff9330b8ea /kernel/indtypes.ml | |
| parent | 5d90e05b35f85607c43888b9adb0319e98a81fb4 (diff) | |
| parent | 8272c4e08f3c045a27d0bcb89a67a167625bf233 (diff) | |
Merge PR #8601: Move bound universe names to abstract contexts
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0346026aa4..20c90bc05a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -268,8 +268,8 @@ let typecheck_inductive env mie = let env' = match mie.mind_entry_universes with | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry ctx -> push_context ctx env - | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env + | Polymorphic_ind_entry (_, ctx) -> push_context ctx env + | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env in let env_params = check_context env' mie.mind_entry_params in let paramsctxt = mie.mind_entry_params in @@ -407,7 +407,7 @@ let typecheck_inductive env mie = match mie.mind_entry_universes with | Monomorphic_ind_entry _ -> () | Polymorphic_ind_entry _ -> () - | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds + | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -851,12 +851,12 @@ let compute_projections (kn, i as ind) mib = let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in + | Polymorphic_ind_entry (nas, ctx) -> + let (inst, auctx) = Univ.abstract_universes nas ctx in let inst = Univ.make_instance_subst inst in (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + | Cumulative_ind_entry (nas, cumi) -> + let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in let inst = Univ.make_instance_subst inst in (inst, Cumulative_ind acumi) |