Module `Declare`

module Hook : sig ... end: Declaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.

One-go, non-interactive declaration API

module CInfo : sig ... end: Information for a single top-level named constant

module Info : sig ... end: Information for a declaration, interactive or not, includes parameters shared by mutual constants

val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t -> opaque:bool -> body:EConstr.t -> Evd.evar_map -> Names.GlobRef.t: Declares a non-interactive constant; body and types will be normalized w.r.t. the passed evar_map sigma. Universes should be handled properly, including minimization and restriction. Note that sigma is checked for unresolved evars, thus you should be careful not to submit open terms

val declare_assumption : name:Names.Id.t -> scope:Locality.locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Entries.parameter_entry -> Names.GlobRef.t

type lemma_possible_guards = int list list

val declare_mutually_recursive : info:Info.t -> cinfo:Constr.t CInfo.t list -> opaque:bool -> ntns:Vernacexpr.decl_notation list -> uctx:UState.t -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option -> Names.GlobRef.t list

Declaration of interactive constants

module OblState : sig ... end: save / save_admitted can update obligations state, so we need to expose the state here

module Proof : sig ... end: Declare.Proof.t Construction of constants using interactive proofs.

low-level, internla API, avoid using unless you have special needs

type 'a proof_entry

Proof entries represent a proof that has been finished, but still not registered with the kernel.

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val definition_entry : ?⁠opaque:bool -> ?⁠using:Names.Id.Set.t -> ?⁠inline:bool -> ?⁠types:Constr.types -> ?⁠univs:Entries.universes_entry -> Constr.constr -> Evd.side_effects proof_entry
val declare_entry : name:Names.Id.t -> scope:Locality.locality -> kind:Decls.logical_kind -> ?⁠hook:Hook.t -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Evd.side_effects proof_entry -> Names.GlobRef.t: XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> typ:Constr.types -> impl:Glob_term.binding_kind -> unit: Declaration of local constructions (Variable/Hypothesis/Local)

type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of Entries.parameter_entry | PrimitiveEntry of Entries.primitive_entry

Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/...

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val prepare_parameter : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -> Evd.evar_map * Entries.parameter_entry

val declare_constant : ?⁠local:Locality.import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> ?⁠typing_flags:Declarations.typing_flags -> Evd.side_effects constant_entry -> 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

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val definition_message : Names.Id.t -> unit: XXX: Scheduled for removal from public API, do not use

val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val check_exists : Names.Id.t -> unit
val build_by_tactic : ?⁠side_eff:bool -> Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t: Semantics of this function is a bit dubious, use with care

Program mode API

Coq's Program mode support. This mode extends declarations of constants and fixpoints with Program Definition and Program Fixpoint to support incremental construction of terms using delayed proofs, called "obligations"

The mode also provides facilities for managing and auto-solving sets of obligations.

The basic code flow of programs/obligations is as follows:

add_definition / add_mutual_definitions are called from the respective Program vernacular command interpretation; at this point the only extra work we do is to prepare the new definition d using RetrieveObl, which consists in turning unsolved evars into obligations. d is not sent to the kernel yet, as it is not complete and cannot be typchecked, but saved in a special data-structure. Auto-solving of obligations is tried at this stage (see below)

next_obligation will retrieve the next obligation (RetrieveObl sorts them by topological order) and will try to solve it. When all obligations are solved, the original constant d is grounded and sent to the kernel for addition to the global environment. Auto-solving of obligations is also triggered on obligation completion.

Solving of obligations: Solved obligations are stored as regular global declarations in the global environment, usually with name constant_obligation_number where constant is the original constant and number is the corresponding (internal) number.

Solving an obligation can trigger a bit of a complex cascaded callback path; closing an obligation can indeed allow all other obligations to be closed, which in turn may trigged the declaration of the original constant. Care must be taken, as this can modify Global.env in arbitrarily ways. Current code takes some care to refresh the env in the proper boundaries, but the invariants remain delicate.

Saving of obligations: as open obligations use the regular proof mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason obligations code is split in two: this file, Obligations, taking care of the top-level vernac commands, and Declare, which is called by `Lemmas` to close an obligation proof and eventually to declare the top-level Programed constant.

module Obls : sig ... end

For internal support, do not use

module Internal : sig ... end