[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, 5 insertions, 6 deletions

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 =