1 files changed, 76 insertions, 0 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
new file mode 100644
index 00000000..c1a673ed
--- /dev/null
+++ b/library/decl_kinds.ml
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*         *   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