Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)

2 files changed, 7 insertions, 2 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d5312c5006..7f4b85fd05 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 c44a17df2a..ca79de404d 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;