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.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'library/lib.mli') 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