Getting rid of AUContext abstraction breakers in Discharge.

6 files changed, 34 insertions, 40 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 28f108a15..154793a32 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -333,9 +333,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in
+  let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie)
+        Discharge.process_inductive info repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
diff --git a/library/lib.ml b/library/lib.ml
index 439f83578..a24d20c68 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -645,3 +645,16 @@ let discharge_con cst =
 
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
+
+let discharge_abstract_universe_context (_, subst, abs_ctx) auctx =
+  let open Univ in
+  let len = LMap.cardinal subst in
+  let rec gen_subst i acc =
+    if i < 0 then acc
+    else
+      let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
+      gen_subst (pred i) acc
+  in
+  let subst = gen_subst (AUContext.size auctx - 1) subst in
+  let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
+  subst, AUContext.union abs_ctx auctx
diff --git a/library/lib.mli b/library/lib.mli
index 38a29f76e..f1c9bfca2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,3 +183,5 @@ val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
+val discharge_abstract_universe_context :
+  abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 5af36fc6b..c4418b5a6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -184,20 +184,6 @@ let subst_class (subst,cl) =
     cl_strict = cl.cl_strict;
     cl_unique = cl.cl_unique }
 
-(** FIXME: share this with Cooking somewhere in a nicely packed API *)
-let lift_abstract_context subst abs_ctx auctx =
-  let open Univ in
-  let len = LMap.cardinal subst in
-  let rec gen_subst i acc =
-    if i < 0 then acc
-    else
-      let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
-      gen_subst (pred i) acc
-  in
-  let subst = gen_subst (AUContext.size auctx - 1) subst in
-  let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
-  subst, AUContext.union abs_ctx auctx
-
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
@@ -232,9 +218,9 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, usubst, uctx = abs_context cl in
+    let ctx, _, _ as info = abs_context cl in
     let ctx, subst = rel_of_variable_context ctx in
-    let usubst, cl_univs' = lift_abstract_context usubst uctx cl.cl_univs in
+    let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
     let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
     let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b6308aba0..474c0b4dd 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -77,42 +77,36 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Type ar.template_level), true
 
-let process_inductive (sechyps,abs_ctx) modlist mib =
+let process_inductive (sechyps,_,_ as info) modlist mib =
+  let sechyps = Lib.named_of_variable_context sechyps in
   let nparams = mib.mind_nparams in
-  let subst, univs =
+  let subst, ind_univs =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+    | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
     | Polymorphic_ind auctx ->
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Polymorphic_ind_entry auctx
     | Cumulative_ind cumi ->
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
   in
+  let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
     Array.map_to_list
       (fun mip ->
 	let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
-	let arity = expmod_constr modlist ty in
-	let arity = Vars.subst_instance_constr subst arity in
-	let lc = Array.map 
-	  (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c))
-	  mip.mind_user_lc 
-	in
+        let arity = discharge ty in
+        let lc = Array.map discharge mip.mind_user_lc  in
 	  (mip.mind_typename,
 	   arity, template,
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map discharge sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let abs_ctx = Univ.instantiate_univ_context abs_ctx in
-  let univs = Univ.UContext.union abs_ctx univs in
-  let ind_univs =
-    match mib.mind_universes with
-    | Monomorphic_ind _ -> Monomorphic_ind_entry univs
-    | Polymorphic_ind _ -> Polymorphic_ind_entry univs
-    | Cumulative_ind _ ->
-      Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index a0dabe2f4..c8c7e3b8b 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,5 +11,4 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
-  -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry