Share API between Discharge and Cooking.

3 files changed, 14 insertions, 14 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index fd1f7df9aa..7fccd4c933 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -53,6 +53,13 @@ let load_constant i ((sp,kn), obj) =
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con obj.cst_kind
 
+let cooking_info segment =
+  let modlist = replacement_context () in
+  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
+  let named_ctx = List.map fst hyps in
+  let abstract = (named_ctx, subst, uctx) in
+  { Opaqueproof.modlist; abstract }
+
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn), obj) =
   (* Never open a local definition *)
@@ -89,14 +96,10 @@ let cache_constant ((sp,kn), obj) =
 let discharge_constant ((sp, kn), obj) =
   let con = Constant.make1 kn in
   let from = Global.lookup_constant con in
-  let modlist = replacement_context () in
-  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in
-  let named_ctx = List.map fst hyps in
-  let abstract = (named_ctx, subst, uctx) in
-  let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in
+  let info = cooking_info (section_segment_of_constant con) in
   (* This is a hack: when leaving a section, we lose the constant definition, so
      we have to store it in the libobject to be able to retrieve it after. *)
-  Some { obj with cst_decl = Some new_decl; }
+  Some { obj with cst_decl = Some { from; info } }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant cst = {
@@ -313,10 +316,8 @@ let cache_inductive ((sp,kn),mie) =
 let discharge_inductive ((sp,kn),mie) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
-  let repl = replacement_context () in
-  let info = section_segment_of_mutual_inductive mind in
-  let hyps = List.map fst info.abstr_ctx in
-  Some (Discharge.process_inductive hyps info.abstr_subst info.abstr_uctx repl mie)
+  let info = cooking_info (section_segment_of_mutual_inductive mind) in
+  Some (Discharge.process_inductive info mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
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