From fa1782e05eeb6f18871d26cc43670d35ed73bf23 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 20:21:49 +0200
Subject: [dumpglob] Move dumpglob-specific data to dumpglob.

The whole business of cst_kind is fishy tho, it seems to me that it
should be removed from the libobject path.
---
 tactics/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index b994585e8a..6a7f728abc 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -53,7 +53,7 @@ let load_constant i ((sp,kn), obj) =
     alreadydeclared (Id.print (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
-  Decls.add_constant_kind con obj.cst_kind
+  Dumpglob.add_constant_kind con obj.cst_kind
 
 let cooking_info segment =
   let modlist = replacement_context () in
@@ -94,7 +94,7 @@ let cache_constant ((sp,kn), obj) =
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
   add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
-  Decls.add_constant_kind (Constant.make1 kn) obj.cst_kind
+  Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
   let con = Constant.make1 kn in
-- 
cgit v1.2.3