aboutsummaryrefslogtreecommitdiff
path: root/library/lib.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-10-16 16:27:53 +0200
committerPierre-Marie Pédrot2019-10-16 16:27:53 +0200
commitcc9856e33fa1a15fe699e8d9cd7b76086563683d (patch)
tree3a51c6466ff40685d2c126a3997390c227b2ce8b /library/lib.mli
parent5d82451d6d6f591ad81919d8e6529cee48474b9e (diff)
parentafd214869f050d07f9774d770c289bdc6e602dfd (diff)
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
Reviewed-by: ejgallego Reviewed-by: ppedrot
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 *)