From fb49af8874d01871ea7ca0bd2a46d135dba27bc2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 11 Jul 2017 18:30:44 +0200
Subject: Getting rid of AUContext abstraction breakers in Discharge.

---
 library/declare.ml |  4 ++--
 library/lib.ml     | 13 +++++++++++++
 library/lib.mli    |  2 ++
 3 files changed, 17 insertions(+), 2 deletions(-)

(limited to 'library')

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