From c3479eceb8e07b37570a80bca9937e3520c61024 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 13 Oct 2019 16:32:15 +0200
Subject: Use kernel info from Global for Lib.sections_{depth,are_opened}

---
 kernel/section.ml  | 2 ++
 kernel/section.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'kernel')

diff --git a/kernel/section.ml b/kernel/section.ml
index babd9fe7a1..a1242f0faf 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -43,6 +43,8 @@ let empty = []
 
 let is_empty = List.is_empty
 
+let depth = List.length
+
 let has_poly_univs = function
   | [] -> false
   | sec :: _ -> sec.has_poly_univs
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 =
-- 
cgit v1.2.3