From fb49af8874d01871ea7ca0bd2a46d135dba27bc2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 18:30:44 +0200 Subject: Getting rid of AUContext abstraction breakers in Discharge. --- library/lib.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'library/lib.ml') 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 -- cgit v1.2.3