diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/discharge.ml | 3 | ||||
| -rw-r--r-- | kernel/discharge.mli | 4 |
2 files changed, 3 insertions, 4 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 diff --git a/kernel/discharge.mli b/kernel/discharge.mli index 3e32a12c3c..1f06c5a734 100644 --- a/kernel/discharge.mli +++ b/kernel/discharge.mli @@ -10,8 +10,6 @@ open Declarations open Entries -open Opaqueproof val process_inductive : - Constr.named_context -> - Univ.Instance.t -> Univ.AUContext.t -> work_list -> mutual_inductive_body -> mutual_inductive_entry + Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_entry |