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 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/section.ml')

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
-- 
cgit v1.2.3