Module Declare

This module provides the functions to declare new variables, parameters, constants and inductive types in the global environment. It also updates some accessory tables such as Nametab (name resolution), Impargs, and Notations.

We provide three main entry points:

Note that the API in this file is still in a state of flux, don't hesitate to contact the maintainers if you have any question.

Additionally, this file does contain some low-level functions, marked as such; these functions are unstable and should not be used unless you already know what they are doing.

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 -> ?using:Vernacexpr.section_subset_expr -> 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_mutual_definitions : info:Info.t -> cinfo:Constr.t CInfo.t list -> opaque:bool -> uctx:UState.t -> bodies:(Constr.t list * Sorts.relevance list) -> possible_guard:Pretyping.possible_guard -> ?using:Vernacexpr.section_subset_expr -> unit -> 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, internal API, avoid using unless you have special needs

type 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

type parameter_entry
type primitive_entry
type symbol_entry
val definition_entry : ?opaque:bool -> ?using:Names.Id.Set.t -> ?inline:bool -> ?types:Constr.types -> ?univs:UState.named_universes_entry -> Constr.constr -> proof_entry
val parameter_entry : ?inline:int -> ?univs:UState.named_universes_entry -> Constr.constr -> parameter_entry
val primitive_entry : ?types:(Constr.types * UState.named_universes_entry) -> CPrimitives.op_or_type -> primitive_entry
val symbol_entry : ?univs:UState.named_universes_entry -> unfold_fix:bool -> Constr.types -> symbol_entry
val declare_entry : name:Names.Id.t -> ?scope:Locality.definition_scope -> kind:Decls.logical_kind -> ?user_warns:Globnames.extended_global_reference UserWarn.with_qf -> ?hook:Hook.t -> impargs:Impargs.manual_implicits -> uctx:UState.t -> 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

type variable_declaration =
| SectionLocalDef of {
clearbody : bool;
entry : proof_entry;
}
| SectionLocalAssum of {
typ : Constr.types;
impl : Glob_term.binding_kind;
univs : UState.named_universes_entry;
}

Declaration of section variables and local definitions

val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> typing_flags:Declarations.typing_flags option -> variable_declaration -> unit

Declaration of local constructions (Variable/Hypothesis/Local)

type constant_entry =
| DefinitionEntry of proof_entry
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
| SymbolEntry of symbol_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 * parameter_entry

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 declare_definition_full : info:Info.t -> cinfo:EConstr.t option CInfo.t -> opaque:bool -> body:EConstr.t -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> Names.GlobRef.t * Univ.ContextSet.t

Like declare_definition but also returns the universes and universe constraints added to the global environment

Declaration messages, for internal use

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 : Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types option * UState.named_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:

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
val is_local_constant : Names.Constant.t -> bool
For internal support, do not use
module Internal : sig ... end