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.
---
 interp/dumpglob.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 53baf137cf..482303d935 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -104,13 +104,20 @@ let type_of_logical_kind = function
       | Corollary -> "thm")
   | IsPrimitive -> "prim"
 
+
+(** Data associated to global parameters and constants *)
+
+let csttab = Summary.ref (Names.Cmap.empty : logical_kind Names.Cmap.t) ~name:"CONSTANT"
+let add_constant_kind kn k = csttab := Names.Cmap.add kn k !csttab
+let constant_kind kn = Names.Cmap.find kn !csttab
+
 let type_of_global_ref gr =
   if Typeclasses.is_class gr then
     "class"
   else
     match gr with
     | Globnames.ConstRef cst ->
-	type_of_logical_kind (Decls.constant_kind cst)
+        type_of_logical_kind (constant_kind cst)
     | Globnames.VarRef v ->
 	"var" ^ type_of_logical_kind (Decls.variable_kind v)
     | Globnames.IndRef ind ->
-- 
cgit v1.2.3