From 4f0607dc76d3981fa67ab6231f2817cd1e6134a5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 10 Dec 2017 04:51:27 +0100
Subject: [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.
---
 intf/decl_kinds.ml | 3 ++-
 intf/vernacexpr.ml | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 1dea6d9e98..b0c1f66613 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 5c9141fd6f..8deddaa5d3 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
-- 
cgit v1.2.3