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}

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index c7c0766587..61321cd605 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -584,7 +584,7 @@ let declare_univ_binders gr pl =
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
 let do_universe ~poly l =
-  let in_section = Lib.sections_are_opened () in
+  let in_section = Global.sections_are_opened () in
   let () =
     if poly && not in_section then
       CErrors.user_err ~hdr:"Constraint"
-- 
cgit v1.2.3