aboutsummaryrefslogtreecommitdiff
path: root/library/lib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.mli')
-rw-r--r--library/lib.mli1
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 *)