Move the Discharge module into the kernel.

7 files changed, 27 insertions, 14 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 7ee7ecb5e8..fd1f7df9aa 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -91,7 +91,8 @@ let discharge_constant ((sp, kn), obj) =
   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 abstract = (named_of_variable_context hyps, subst, uctx) 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
   (* 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. *)
@@ -314,7 +315,8 @@ let discharge_inductive ((sp,kn),mie) =
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
   let info = section_segment_of_mutual_inductive mind in
-  Some (Discharge.process_inductive info repl mie)
+  let hyps = List.map fst info.abstr_ctx in
+  Some (Discharge.process_inductive hyps info.abstr_subst info.abstr_uctx repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 1262dbb181..b65a171ef9 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -16,5 +16,4 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Discharge
 Declare
diff --git a/interp/discharge.ml b/kernel/discharge.ml
index 1efd13adb1..e7e84f14d0 100644
--- a/interp/discharge.ml
+++ b/kernel/discharge.ml
@@ -30,6 +30,9 @@ open Entries
      I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
 *)
 
+let it_mkNamedProd_wo_LetIn b d =
+  List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d
+
 let abstract_inductive decls nparamdecls inds =
   let ntyp = List.length inds in
   let ndecls = Context.Named.length decls in
@@ -40,8 +43,8 @@ let abstract_inductive decls nparamdecls inds =
     List.map
       (function (tname,arity,template,cnames,lc) ->
 	let lc' = List.map (substl subs) lc in
-	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in
-	let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in
+        let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in
+        let arity' = it_mkNamedProd_wo_LetIn arity decls in
         (tname,arity',template,cnames,lc''))
       	inds in
   let nparamdecls' = nparamdecls + Array.length args in
@@ -71,21 +74,32 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
 
-let process_inductive info modlist mib =
-  let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in
+let dummy_variance = let open Entries in function
+  | Monomorphic_entry _ -> assert false
+  | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
+
+let discharge_abstract_universe_context subst abs_ctx auctx =
+  let open Univ in
+  let ainst = make_abstract_instance auctx in
+  let subst = Instance.append subst ainst in
+  let subst = make_instance_subst subst in
+  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 nparamdecls = Context.Rel.length mib.mind_params_ctxt in
   let subst, ind_univs =
     match mib.mind_universes with
     | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
     | Polymorphic auctx ->
-      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in
       let nas = Univ.AUContext.names auctx in
       let auctx = Univ.AUContext.repr auctx in
       subst, Polymorphic_entry (nas, auctx)
   in
   let variance = match mib.mind_variance with
     | None -> None
-    | Some _ -> Some (InferCumulativity.dummy_variance ind_univs)
+    | Some _ -> Some (dummy_variance ind_univs)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
diff --git a/interp/discharge.mli b/kernel/discharge.mli
index f7408937cf..3e32a12c3c 100644
--- a/interp/discharge.mli
+++ b/kernel/discharge.mli
@@ -13,4 +13,5 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Constr.named_context ->
+  Univ.Instance.t -> Univ.AUContext.t -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 59c1d5890f..238cbba425 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -48,4 +48,5 @@ Term_typing
 Subtyping
 Mod_typing
 Nativelibrary
+Discharge
 Safe_typing
diff --git a/library/lib.ml b/library/lib.ml
index 4be288ed20..daa41eca65 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -474,9 +474,6 @@ let extract_hyps (secs,ohyps) =
 let instance_from_variable_context =
   List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
 
-let named_of_variable_context =
-  List.map fst
-
 let name_instance inst =
   (* FIXME: this should probably be done at an upper level, by storing the
      name information in the section data structure. *)
diff --git a/library/lib.mli b/library/lib.mli
index 5da76961a6..c19c3bf7fa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,7 +168,6 @@ type abstr_info = private {
 }
 
 val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Constr.named_context
 
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info