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!

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?

yes

Last updated: Oct 13 2024 at 01:02 UTC