diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/lib.mli b/library/lib.mli index 9933b762ba..686e6a0e2d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,12 +183,12 @@ 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 -val discharge_con : Constant.t -> Constant.t +(* XXX Why can't we use the kernel functions ? *) + val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t -val discharge_global : GlobRef.t -> GlobRef.t -val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t |