[search] Don't use ad-hoc Dumpglob table for Search

This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.

4 files changed, 15 insertions, 8 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index df75e121d8..12a261517f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -535,10 +535,13 @@ module Internal = struct
     ; proof_entry_type = Some typ
     }, args
 
-  type nonrec constant_obj = constant_obj
+  module Constant = struct
+    type t = constant_obj
+    let tag = objConstant
+    let kind obj = obj.cst_kind
+  end
 
   let objVariable = objVariable
-  let objConstant = objConstant
 
 end
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index adb5bd026f..c5a8afbad5 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -556,9 +556,13 @@ end
 
 module Internal : sig
 
-  type constant_obj
+  (* Liboject exports *)
+  module Constant : sig
+    type t
+    val tag : t Libobject.Dyn.tag
+    val kind : t -> Decls.logical_kind
+  end
 
-  val objConstant : constant_obj Libobject.Dyn.tag
   val objVariable : unit Libobject.Dyn.tag
 
 end
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 176ddd6c5b..2b46542287 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -688,7 +688,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) =
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       end @@
-      DynHandle.add Declare.Internal.objConstant begin fun _ ->
+      DynHandle.add Declare.Internal.Constant.tag begin fun _ ->
           Some (print_constant with_values sep (Constant.make1 kn) None)
       end @@
       DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
@@ -796,7 +796,7 @@ let print_full_pure_context env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
     let handler =
-      DynHandleF.add Declare.Internal.objConstant begin fun _ ->
+      DynHandleF.add Declare.Internal.Constant.tag begin fun _ ->
           let con = Global.constant_of_delta_kn kn in
           let cb = Global.lookup_constant con in
           let typ = cb.const_type in
diff --git a/vernac/search.ml b/vernac/search.ml
index 2a21184c1e..abefeab779 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -79,11 +79,11 @@ let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> co
   let iter_obj (sp, kn) lobj = match lobj with
     | AtomicObject o ->
       let handler =
-        DynHandle.add Declare.Internal.objConstant begin fun _ ->
+        DynHandle.add Declare.Internal.Constant.tag begin fun obj ->
           let cst = Global.constant_of_delta_kn kn in
           let gr = GlobRef.ConstRef cst in
           let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
-          let kind = Dumpglob.constant_kind cst in
+          let kind = Declare.Internal.Constant.kind obj in
           fn gr (Some kind) env typ
         end @@
         DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->