diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 18:30:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | fb49af8874d01871ea7ca0bd2a46d135dba27bc2 (patch) | |
| tree | 5c7ebcc651109d70bb8073a7b98174de10221648 /library/lib.mli | |
| parent | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (diff) | |
Getting rid of AUContext abstraction breakers in Discharge.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |