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

5 files changed, 13 insertions, 17 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
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