diff options
| author | Gaëtan Gilbert | 2019-10-13 16:32:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | c3479eceb8e07b37570a80bca9937e3520c61024 (patch) | |
| tree | 136a1773ad9b1bd1cdecd3db26ca0cc64f4516cf /kernel/section.mli | |
| parent | 26e8b5a545bcf2209d56494ccf4afe143f761fd7 (diff) | |
Use kernel info from Global for Lib.sections_{depth,are_opened}
Diffstat (limited to 'kernel/section.mli')
| -rw-r--r-- | kernel/section.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/section.mli b/kernel/section.mli index 56b4d9ba8f..ec863b3b90 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -21,6 +21,9 @@ val empty : 'a t val is_empty : 'a t -> bool (** Checks whether there is no opened section *) +val depth : 'a t -> int +(** Number of nested sections (0 if no sections are open) *) + (** {6 Manipulating sections} *) type section_entry = |