Stream: Coq devs & plugin devs

Topic: Changes to Declarations.universes from Coq 8.9 to 8.10


view this post on Zulip Arpan Agrawal (Aug 07 2023 at 18:25):

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?
Thanks!

view this post on Zulip Gaëtan Gilbert (Aug 07 2023 at 19:12):

you're not doing anything interesting with the variance info so I don't see the problem

view this post on Zulip Arpan Agrawal (Aug 07 2023 at 19:23):

Does that mean we just don't create an entry for that case anymore?

view this post on Zulip Gaëtan Gilbert (Aug 07 2023 at 19:24):

yes


Last updated: Jun 13 2024 at 04:03 UTC