From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 intf/decl_kinds.ml | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 intf/decl_kinds.ml

(limited to 'intf/decl_kinds.ml')

diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
new file mode 100644
index 00000000..0d328531
--- /dev/null
+++ b/intf/decl_kinds.ml
@@ -0,0 +1,87 @@
+(************************************************************************)
+(*         *   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"]
-- 
cgit v1.2.3