diff options
Diffstat (limited to 'kernel/discharge.ml')
| -rw-r--r-- | kernel/discharge.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/discharge.ml b/kernel/discharge.ml index e7e84f14d0..f75ff8454a 100644 --- a/kernel/discharge.ml +++ b/kernel/discharge.ml @@ -86,7 +86,8 @@ let discharge_abstract_universe_context subst abs_ctx auctx = let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in subst, AUContext.union abs_ctx auctx -let process_inductive section_decls subst abs_uctx modlist mib = +let process_inductive { Opaqueproof.modlist; abstract } mib = + let (section_decls, subst, abs_uctx) = abstract in let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with |