diff options
| author | Gaëtan Gilbert | 2018-09-14 12:59:52 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-27 13:28:33 +0200 |
| commit | 2566d45fcc05c1cd80ba2ac16ef342e7f145f01a (patch) | |
| tree | da9b8f3d9574f467ae494dba4acb703f726c06c9 /library/lib.mli | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Fix #8478: Undeclared universe anomaly with sections
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
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 9933b762ba..a7d21060e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,6 +183,8 @@ val add_section_kn : Decl_kinds.polymorphic -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list +val is_polymorphic_univ : Univ.Level.t -> bool + (** {6 Discharge: decrease the section level if in the current section } *) val discharge_kn : MutInd.t -> MutInd.t |