[api] Refactor most of `Decl_kinds`

We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.

The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.

Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.

IMO this needs more work, but this should be a good start.

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 56ed406e2f..b32b27ebeb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -127,13 +127,13 @@ let save id const ?hook uctx scope kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match scope with
     | Discharge ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Decls.logical_kind_of_goal_kind kind in
         let c = SectionLocalDef const in
         let _ = declare_variable id (Lib.cwd(), c, k) in
         VarRef id
     | Global local ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
-        let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
+        let k = Decls.logical_kind_of_goal_kind kind in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });