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}

---
 vernac/comPrimitive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comPrimitive.ml')

diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index 06fafddafb..b66ff876d3 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 let do_primitive id prim typopt =
-  if Lib.sections_are_opened () then
+  if Global.sections_are_opened () then
     CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
   if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
   let env = Global.env () in
-- 
cgit v1.2.3