1 files changed, 0 insertions, 87 deletions
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
deleted file mode 100644
index 0d328531..00000000
--- a/intf/decl_kinds.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Informal mathematical status of declarations *)
-
-type discharge = DoDischarge | NoDischarge
-
-type locality = Discharge | Local | Global
-
-type binding_kind = Explicit | Implicit
-
-type polymorphic = bool
-
-type private_flag = bool
-
-type cumulative_inductive_flag = bool
-
-type theorem_kind =
-  | Theorem
-  | Lemma
-  | Fact
-  | Remark
-  | Property
-  | Proposition
-  | Corollary
-
-type definition_object_kind =
-  | Definition
-  | Coercion
-  | SubClass
-  | CanonicalStructure
-  | Example
-  | Fixpoint
-  | CoFixpoint
-  | Scheme
-  | StructureComponent
-  | IdentityCoercion
-  | Instance
-  | Method
-  | Let
-
-type assumption_object_kind = Definitional | Logical | Conjectural
-
-(* [assumption_kind]
-
-                |  Local      | Global
-   ------------------------------------
-   Definitional |  Variable   | Parameter
-   Logical      |  Hypothesis | Axiom
-
-*)
-type assumption_kind = locality * polymorphic * assumption_object_kind
-
-type definition_kind = locality * polymorphic * definition_object_kind
-
-(** Kinds used in proofs *)
-
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
-
-type goal_kind = locality * polymorphic * goal_object_kind
-
-(** Kinds used in library *)
-
-type logical_kind =
-  | IsAssumption of assumption_object_kind
-  | IsDefinition of definition_object_kind
-  | IsProof of theorem_kind
-
-(** Recursive power of type declarations *)
-
-type recursivity_kind = Declarations.recursivity_kind =
-  | Finite (** = inductive *)
-      [@ocaml.deprecated "Please use [Declarations.Finite"]
-  | CoFinite (** = coinductive *)
-      [@ocaml.deprecated "Please use [Declarations.CoFinite"]
-  | BiFinite (** = non-recursive, like in "Record" definitions *)
-      [@ocaml.deprecated "Please use [Declarations.BiFinite"]
-[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"]