diff options
Diffstat (limited to 'interp/discharge.ml')
| -rw-r--r-- | interp/discharge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/discharge.ml b/interp/discharge.ml index 75bfca307..710f88c3f 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -92,7 +92,7 @@ let process_inductive info modlist mib = let auctx = Univ.ACumulativityInfo.univ_context cumi in let subst, auctx = Lib.discharge_abstract_universe_context info auctx in let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx) + subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = |