2 files changed, 5 insertions, 0 deletions
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 =