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

10 files changed, 22 insertions, 24 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e34150f2b3..780cf4af21 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let poly = false in
-  let kind = Decl_kinds.(DefinitionBody Definition) in
+  let kind = Decls.(DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f773b2c39e..6a5307d8f5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
   let info = Lemmas.Info.make
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+      ~kind:(Decls.(Proof Theorem)) () in
 
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3bab750534..87910eeae7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -371,7 +371,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
           Declare.declare_constant
             name
             (Declare.DefinitionEntry ce,
-             Decl_kinds.IsDefinition (Decl_kinds.Scheme))
+             Decls.(IsDefinition Scheme))
         );
         Declare.definition_message name;
         names := name :: !names
@@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -638,7 +638,7 @@ let build_scheme fas =
        ignore
          (Declare.declare_constant
             princ_id
-            (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+            (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem)));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d305a58ccc..9a9e0b9692 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~name:fname
         ~poly:false
         ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-        ~kind:Decl_kinds.Definition pl
+        ~kind:Decls.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
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 });
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 45d332031f..1758efe584 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -48,7 +48,7 @@ val save
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> DeclareDef.locality
-  -> Decl_kinds.goal_object_kind
+  -> Decls.goal_object_kind
   -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 86defb2f2f..153b27c855 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+             ~kind:(Decls.(Proof Theorem)) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
              ~poly:false
@@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_complete_id f_id in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:Decl_kinds.(Proof Theorem) () in
+             ~kind:Decls.(Proof Theorem) () in
          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
              sigma (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d38e28c0e7..0398acf242 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -30,7 +30,6 @@ open Tacmach
 open Tactics
 open Nametab
 open Declare
-open Decl_kinds
 open Tacred
 open Goal
 open Glob_term
@@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
     let body = EConstr.Unsafe.to_constr body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
+let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(Proof Lemma))
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1411,7 +1410,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~sign:(Environ.named_context_val env)
@@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
     let univs = Evd.univ_entry ~poly:false evd in
-    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
+    declare_fun functional_id Decls.(IsDefinition Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
   let evd = Evd.from_env (Global.env ()) in
@@ -1549,7 +1548,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook { DeclareDef.Hook.S.uctx ; _ } =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
-    let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+    let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in
     let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
     (*     message "start second proof"; *)
     let stop =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 19866df8e3..22ad75b784 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1901,8 +1901,8 @@ let declare_projection n instance_id r =
   let cst = 
     Declare.definition_entry ~types:typ ~univs term
   in
-    ignore(Declare.declare_constant n 
-           (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+    ignore(Declare.declare_constant n
+           (Declare.DefinitionEntry cst, Decls.(IsDefinition Definition)))
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1981,7 +1981,7 @@ let add_morphism_as_parameter atts m n : unit =
   let cst = Declare.declare_constant instance_id
       (Declare.ParameterEntry
          (None,(instance,uctx),None),
-       Decl_kinds.IsAssumption Decl_kinds.Logical)
+       Decls.(IsAssumption Logical))
   in
   Classes.add_instance (Classes.mk_instance
                   (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
@@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let poly = atts.polymorphic in
-  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let kind = Decls.(DefinitionBody Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
     | Globnames.ConstRef cst ->
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 33798c43c8..3d6bfda0b2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -29,7 +29,6 @@ open Tacinterp
 open Libobject
 open Printer
 open Declare
-open Decl_kinds
 open Entries
 open Newring_ast
 open Proofview.Notations
@@ -158,7 +157,7 @@ let decl_constant na univs c =
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
-	     IsProof Lemma))
+             Decls.(IsProof Lemma)))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =