From 787dd2e37c80dd75b09a3c2805bfcbfa4b821a68 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 08:20:15 +0200
Subject: Share API between Discharge and Cooking.

---
 kernel/discharge.ml  | 3 ++-
 kernel/discharge.mli | 4 +---
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3