diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index 59d77480e9..cef50a5f3b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool +[@@ocaml.deprecated "Use Global.sections_are_opened"] val sections_depth : unit -> int (** Are we inside an opened module type *) |
