I have this function in a plugin (Coq 8.9):
let make_ind_univs_entry = function | Monomorphic_ind univ_ctx_set -> let univ_ctx = Univ.UContext.empty in (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx) | Polymorphic_ind abs_univ_ctx -> let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in (Entries.Polymorphic_ind_entry univ_ctx, univ_ctx) | Cumulative_ind abs_univ_cumul -> let abs_univ_ctx = Univ.ACumulativityInfo.univ_context abs_univ_cumul in let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in let univ_var = Univ.ACumulativityInfo.variance abs_univ_cumul in let univ_cumul = Univ.CumulativityInfo.make (univ_ctx, univ_var) in (Entries.Cumulative_ind_entry univ_cumul, univ_ctx)
When trying to port to Coq 8.10, I run into the issue that the
Cumulative_ind constructor no longer exists and has been replaced with mind_variance. Can someone please help me with this?
you're not doing anything interesting with the variance info so I don't see the problem
Does that mean we just don't create an entry for that case anymore?
Last updated: Nov 29 2023 at 21:01 UTC