[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.

4 files changed, 11 insertions, 15 deletions

diff --git a/interp/decls.ml b/interp/decls.ml
index 933aa774b4..52685e0666 100644
--- a/interp/decls.ml
+++ b/interp/decls.ml
@@ -92,11 +92,3 @@ let variable_secpath id =
   make_qualid dir id
 
 let variable_exists id = Id.Map.mem id !vartab
-
-(** Datas associated to global parameters and constants *)
-
-let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
-
-let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
-
-let constant_kind kn = Cmap.find kn !csttab
diff --git a/interp/decls.mli b/interp/decls.mli
index 570f03bbce..ce29197891 100644
--- a/interp/decls.mli
+++ b/interp/decls.mli
@@ -92,9 +92,3 @@ val variable_opacity : variable -> bool
 val variable_context : variable -> Univ.ContextSet.t
 val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
-
-(** Registration and access to the table of constants *)
-
-(* Only used in dumpglob *)
-val add_constant_kind : Constant.t -> logical_kind -> unit
-val constant_kind : Constant.t -> logical_kind
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 ->
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 18955985a0..e0308b8afc 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -45,3 +45,6 @@ val dump_constraint : Names.lname -> bool -> string -> unit
 val dump_string : string -> unit
 
 val type_of_global_ref : Names.GlobRef.t -> string
+
+(** Registration of constant information *)
+val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit