Module Decls

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
| Context

Kinds used in library

type logical_kind =
| IsPrimitive
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind

This module manages non-kernel informations about declarations. It is either non-logical informations or logical informations that have no place to be (yet) in the kernel

Registration and access to the table of variable

type variable_data = {
opaque : bool;
kind : logical_kind;
}
val add_variable_data : Names.variable -> variable_data -> unit
val variable_secpath : Names.variable -> Libnames.qualid
val variable_kind : Names.variable -> logical_kind
val variable_opacity : Names.variable -> bool
val variable_exists : Names.variable -> bool