Module Decl_kinds

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
type assumption_kind = locality * polymorphic * assumption_object_kind
type definition_kind = locality * polymorphic * definition_object_kind
type goal_object_kind =
| DefinitionBody of definition_object_kind
| Proof of theorem_kind
type goal_kind = locality * polymorphic * goal_object_kind
type logical_kind =
| IsPrimitive
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind