Module Declare

This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions will add the entries in the global environment (module Global), will register the declarations in the library (module Lib) --- so that the reset works properly --- and will fill some global tables such as Nametab and Impargs.

type section_variable_entry =
| SectionLocalDef of Safe_typing.private_constants Entries.definition_entry
| SectionLocalAssum of Constr.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool

Implicit status

type variable_declaration = Names.DirPath.t * section_variable_entry * Decl_kinds.logical_kind
val declare_variable : Names.variable -> variable_declaration -> Libobject.object_name
type constant_declaration = Safe_typing.private_constants Entries.constant_entry * Decl_kinds.logical_kind
type internal_flag =
| UserAutomaticRequest
| InternalTacticRequest
| UserIndividualRequest
val definition_entry : ?⁠fix_exn:Future.fix_exn -> ?⁠opaque:bool -> ?⁠inline:bool -> ?⁠types:Constr.types -> ?⁠univs:Entries.universes_entry -> ?⁠eff:Safe_typing.private_constants -> Constr.constr -> Safe_typing.private_constants Entries.definition_entry
val declare_constant : ?⁠internal:internal_flag -> ?⁠local:bool -> Names.Id.t -> ?⁠export_seff:bool -> constant_declaration -> Names.Constant.t

declare_constant id cd declares a global declaration (constant/parameter) with name id in the current section; it returns the full path of the declaration

internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent

val declare_definition : ?⁠internal:internal_flag -> ?⁠opaque:bool -> ?⁠kind:Decl_kinds.definition_object_kind -> ?⁠local:bool -> Names.Id.t -> ?⁠types:Constr.constr -> Constr.constr Entries.in_universes_entry -> Names.Constant.t
val set_declare_scheme : (string -> (Names.inductive * Names.Constant.t) array -> unit) -> unit

Since transparent constants' side effects are globally declared, we * need that

val declare_mind : Entries.mutual_inductive_entry -> Libobject.object_name * bool

declare_mind me declares a block of inductive types with their constructors in the current section; it returns the path of the whole block and a boolean indicating if it is a primitive record.

val definition_message : Names.Id.t -> unit
val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val cofixpoint_message : Names.Id.t list -> unit
val recursive_message : bool -> int array option -> Names.Id.t list -> unit
val exists_name : Names.Id.t -> bool
val declare_univ_binders : Names.GlobRef.t -> UnivNames.universe_binders -> unit

Global universe contexts, names and constraints

val declare_universe_context : Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
val do_universe : Decl_kinds.polymorphic -> Names.lident list -> unit
val do_constraint : Decl_kinds.polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit