diff options
| author | Pierre-Marie Pédrot | 2019-05-20 08:20:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-26 00:08:58 +0200 |
| commit | 787dd2e37c80dd75b09a3c2805bfcbfa4b821a68 (patch) | |
| tree | 4ead8b151cea0c030969c2993444bd4364e93b50 /kernel | |
| parent | a21e1bb60f579baec910d4c3d8e8434501470b6d (diff) | |
Share API between Discharge and Cooking.
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 |