[api] Remove kernel dependency on intf (Decl_kind)

We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.

7 files changed, 83 insertions, 71 deletions

diff --git a/API/API.mli b/API/API.mli
index abbdf22b9..c61dc4d90 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1293,65 +1293,6 @@ sig
   type to_patch_substituted
 end
 
-module Decl_kinds :
-sig
-  type polymorphic = bool
-  type cumulative_inductive_flag = bool
-  type recursivity_kind =
-    | Finite
-    | CoFinite
-    | BiFinite
-
-  type discharge =
-    | DoDischarge
-    | NoDischarge
-
-  type locality =
-    | Discharge
-    | Local
-    | Global
-
-  type definition_object_kind =
-    | Definition
-    | Coercion
-    | SubClass
-    | CanonicalStructure
-    | Example
-    | Fixpoint
-    | CoFixpoint
-    | Scheme
-    | StructureComponent
-    | IdentityCoercion
-    | Instance
-    | Method
-    | Let
-  type theorem_kind =
-    | Theorem
-    | Lemma
-    | Fact
-    | Remark
-    | Property
-    | Proposition
-    | Corollary
-  type goal_object_kind =
-    | DefinitionBody of definition_object_kind
-    | Proof of theorem_kind
-  type goal_kind = locality * polymorphic * goal_object_kind
-  type assumption_object_kind =
-    | Definitional
-    | Logical
-    | Conjectural
-  type logical_kind =
-    | IsAssumption of assumption_object_kind
-    | IsDefinition of definition_object_kind
-    | IsProof of theorem_kind
-  type binding_kind =
-    | Explicit
-    | Implicit
-  type private_flag = bool
-  type definition_kind = locality * polymorphic * definition_object_kind
-end
-
 module Retroknowledge :
 sig
   type action
@@ -1501,10 +1442,15 @@ sig
 
   type record_body = (Id.t * Constant.t array * projection_body array) option
 
+  type recursivity_kind =
+    | Finite
+    | CoFinite
+    | BiFinite
+
   type mutual_inductive_body = {
         mind_packets : one_inductive_body array;
         mind_record : record_body option;
-        mind_finite : Decl_kinds.recursivity_kind;
+        mind_finite : recursivity_kind;
         mind_ntypes : int;
         mind_hyps : Context.Named.t;
         mind_nparams : int;
@@ -1578,7 +1524,7 @@ sig
     (** Some (Some id): primitive record with id the binder name of the record
         in projections.
         Some None: non-primitive record *)
-    mind_entry_finite : Decl_kinds.recursivity_kind;
+    mind_entry_finite : Declarations.recursivity_kind;
     mind_entry_params : (Id.t * local_entry) list;
     mind_entry_inds : one_inductive_entry list;
     mind_entry_universes : inductive_universes;
@@ -2210,6 +2156,66 @@ sig
          | SubEvar of Evar.t
 end
 
+module Decl_kinds :
+sig
+  type polymorphic = bool
+  type cumulative_inductive_flag = bool
+  type recursivity_kind = Declarations.recursivity_kind =
+    | Finite
+    | CoFinite
+    | BiFinite
+  [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
+
+  type discharge =
+    | DoDischarge
+    | NoDischarge
+
+  type locality =
+    | Discharge
+    | Local
+    | Global
+
+  type definition_object_kind =
+    | Definition
+    | Coercion
+    | SubClass
+    | CanonicalStructure
+    | Example
+    | Fixpoint
+    | CoFixpoint
+    | Scheme
+    | StructureComponent
+    | IdentityCoercion
+    | Instance
+    | Method
+    | Let
+  type theorem_kind =
+    | Theorem
+    | Lemma
+    | Fact
+    | Remark
+    | Property
+    | Proposition
+    | Corollary
+  type goal_object_kind =
+    | DefinitionBody of definition_object_kind
+    | Proof of theorem_kind
+  type goal_kind = locality * polymorphic * goal_object_kind
+  type assumption_object_kind =
+    | Definitional
+    | Logical
+    | Conjectural
+  type logical_kind =
+    | IsAssumption of assumption_object_kind
+    | IsDefinition of definition_object_kind
+    | IsProof of theorem_kind
+  type binding_kind =
+    | Explicit
+    | Implicit
+  type private_flag = bool
+  type definition_kind = locality * polymorphic * definition_object_kind
+end
+
 module Glob_term :
 sig
   type 'a cases_pattern_r =
@@ -3999,7 +4005,7 @@ sig
 
   type instance_flag  = bool option
   type coercion_flag = bool
-  type inductive_flag = Decl_kinds.recursivity_kind
+  type inductive_flag = Declarations.recursivity_kind
   type lname = Names.Name.t Loc.located
   type lident = Names.Id.t Loc.located
   type opacity_flag =
@@ -6070,7 +6076,7 @@ sig
 
   val do_mutual_inductive :
     (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
-    Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit
+    Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit
 
   val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
     Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
@@ -6096,7 +6102,7 @@ sig
     structured_inductive_expr -> Vernacexpr.decl_notation list ->
     Decl_kinds.cumulative_inductive_flag ->
     Decl_kinds.polymorphic ->
-    Decl_kinds.private_flag -> Decl_kinds.recursivity_kind ->
+    Decl_kinds.private_flag -> Declarations.recursivity_kind ->
     Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
 
   val declare_mutual_inductive_with_eliminations :
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 1dea6d9e9..b0c1f6661 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -75,7 +75,8 @@ type logical_kind =
 
 (** Recursive power of type declarations *)
 
-type recursivity_kind =
+type recursivity_kind = Declarations.recursivity_kind =
   | Finite (** = inductive *)
   | CoFinite (** = coinductive *)
   | BiFinite (** = non-recursive, like in "Record" definitions *)
+[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 5c9141fd6..8deddaa5d 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -145,7 +145,7 @@ type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
-type inductive_flag = Decl_kinds.recursivity_kind
+type inductive_flag = Declarations.recursivity_kind
 type onlyparsing_flag = Flags.compat_version option
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d5312c500..7f4b85fd0 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -172,13 +172,18 @@ type abstract_inductive_universes =
   | Polymorphic_ind of Univ.AUContext.t
   | Cumulative_ind of Univ.ACumulativityInfo.t
 
+type recursivity_kind =
+  | Finite (** = inductive *)
+  | CoFinite (** = coinductive *)
+  | BiFinite (** = non-recursive, like in "Record" definitions *)
+
 type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
     mind_record : record_body option; (** The record information *)
 
-    mind_finite : Decl_kinds.recursivity_kind;  (** Whether the type is inductive or coinductive *)
+    mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
     mind_ntypes : int;  (** Number of types in the block *)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c44a17df2..ca79de404 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -51,7 +51,7 @@ type mutual_inductive_entry = {
   (** Some (Some id): primitive record with id the binder name of the record
       in projections.
       Some None: non-primitive record *)
-  mind_entry_finite : Decl_kinds.recursivity_kind;
+  mind_entry_finite : Declarations.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : inductive_universes;
diff --git a/vernac/command.mli b/vernac/command.mli
index a1f916c78..c7342e6da 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -82,7 +82,7 @@ type one_inductive_impls =
 
 val interp_mutual_inductive :
   structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> Decl_kinds.recursivity_kind ->
+  polymorphic -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
 
 (** Registering a mutual inductive definition together with its
@@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations :
 
 val do_mutual_inductive :
   (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit
+  polymorphic -> private_flag -> Declarations.recursivity_kind -> unit
 
 (** {6 Fixpoints and cofixpoints} *)
 
diff --git a/vernac/record.mli b/vernac/record.mli
index 9fdd5e1c4..e632e7bbf 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -15,7 +15,7 @@ val primitive_flag : bool ref
 
 val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
-  Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
+  Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference