diff options
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 |