diff options
Diffstat (limited to 'vernac/search.ml')
| -rw-r--r-- | vernac/search.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 _ -> |