diff options
| author | Pierre-Marie Pédrot | 2018-09-27 14:23:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-09 14:10:27 +0100 |
| commit | 601ce3738253e4bb197900ee6dad271c4e3666d6 (patch) | |
| tree | c4164f53de30589a26a147f548b8693875971027 /kernel/indtypes.ml | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
Adding universe names to polymorphic entry instances.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0346026aa4..2d74f99c15 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,14 @@ 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 -> + | Polymorphic_ind_entry (nas, ctx) -> + let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in let (inst, auctx) = Univ.abstract_universes ctx in let inst = Univ.make_instance_subst inst in (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (nas, cumi) -> let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let () = assert (Int.equal (List.length nas) (Instance.length inst)) in let inst = Univ.make_instance_subst inst in (inst, Cumulative_ind acumi) |