Module Declare

module Proof : sig ... end

Declare.Proof.t Construction of constants using interactive proofs.

type opacity_flag = Vernacexpr.opacity_flag =
| Opaque
| Transparent
val start_proof : name:Names.Id.t -> udecl:UState.universe_decl -> poly:bool -> Evd.evar_map -> (Environ.env * EConstr.types) list -> Proof.t

start_proof ~name ~udecl ~poly sigma goals starts a proof of name name with goals goals (a list of pairs of environment and conclusion); poly determines if the proof is universe polymorphic. The proof is started in the evar map sigma (which can typically contain universe constraints), and with universe bindings udecl.

val start_dependent_proof : name:Names.Id.t -> udecl:UState.universe_decl -> poly:bool -> Proofview.telescope -> Proof.t

Like start_proof except that there may be dependencies between initial goals.

type 'a proof_entry = private {
proof_entry_body : 'a Entries.const_entry_body;
proof_entry_secctx : Names.Id.Set.t option;
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
proof_entry_universes : Entries.universes_entry;
proof_entry_opaque : bool;
proof_entry_inline_code : bool;
}

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

XXX: Scheduled for removal from public API, don't rely on it

type proof_object = private {
name : Names.Id.t;

name of the proof

entries : Evd.side_effects proof_entry list;

list of the proof terms (in a form suitable for definitions).

uctx : UState.t;

universe state

}

XXX: Scheduled for removal from public API, don't rely on it

val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
type variable_declaration =
| SectionLocalDef of Evd.side_effects proof_entry
| SectionLocalAssum of {
typ : Constr.types;
impl : Glob_term.binding_kind;
}

XXX: Scheduled for removal from public API, don't rely on it

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

XXX: Scheduled for removal from public API, don't rely on it

val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> variable_declaration -> unit
val definition_entry : ?⁠fix_exn:Future.fix_exn -> ?⁠opaque:bool -> ?⁠inline:bool -> ?⁠feedback_id:Stateid.t -> ?⁠section_vars:Names.Id.Set.t -> ?⁠types:Constr.types -> ?⁠univs:Entries.universes_entry -> ?⁠eff:Evd.side_effects -> ?⁠univsbody:Univ.ContextSet.t -> Constr.constr -> Evd.side_effects proof_entry

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

XXX: Scheduled for removal from public API, use `DeclareDef` instead

type import_status =
| ImportDefaultBehavior
| ImportNeedQualified
val declare_constant : ?⁠local:import_status -> name:Names.Id.t -> kind:Decls.logical_kind -> 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

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

XXX: Scheduled for removal from public API, use `DeclareDef` instead

val inline_private_constants : uctx:UState.t -> Environ.env -> Evd.side_effects proof_entry -> Constr.t * UState.t

inline_private_constants ~sideff ~uctx env ce will inline the constants in ce's body and return the body plus the updated UState.t.

XXX: Scheduled for removal from public API, don't rely on it

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
For legacy support, do not use
module Internal : sig ... end
type closed_proof_output
val return_proof : Proof.t -> closed_proof_output

Requires a complete proof.

val return_partial_proof : Proof.t -> closed_proof_output

An incomplete proof is allowed (no error), and a warn is given if the proof is complete.

val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool

by tac applies tactic tac to the 1st subgoal of the current focused proof. Returns false if an unsafe tactic has been used.

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
Helpers to obtain proof state when in an interactive proof
val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env
val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env

get_current_goal_context () works as get_goal_context 1

val get_current_context : Proof.t -> Evd.evar_map * Environ.env

get_current_context () returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map.

val build_constant_by_tactic : name:Names.Id.t -> ?⁠opaque:opacity_flag -> uctx:UState.t -> sign:Environ.named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic -> Evd.side_effects proof_entry * bool * UState.t

Temporarily re-exported for 3rd party code; don't use

val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
type locality =
| Discharge
| Global of import_status
module Hook : sig ... end

Declaration hooks

val declare_entry : name:Names.Id.t -> scope:locality -> kind:Decls.logical_kind -> ?⁠hook:Hook.t -> ?⁠obls:(Names.Id.t * Constr.t) list -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Evd.side_effects proof_entry -> Names.GlobRef.t

Declare an interactively-defined constant

val declare_definition : name:Names.Id.t -> scope:locality -> kind:Decls.logical_kind -> opaque:bool -> impargs:Impargs.manual_implicits -> udecl:UState.universe_decl -> ?⁠hook:Hook.t -> ?⁠obls:(Names.Id.t * Constr.t) list -> poly:bool -> ?⁠inline:bool -> types:EConstr.t option -> body:EConstr.t -> ?⁠fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> 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 or evar maps with stale, unresolved existentials

val declare_assumption : ?⁠fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> name:Names.Id.t -> scope:locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Entries.parameter_entry -> Names.GlobRef.t
module Recthm : sig ... end
val declare_mutually_recursive : opaque:bool -> scope:locality -> kind:Decls.logical_kind -> poly:bool -> uctx:UState.t -> udecl:UState.universe_decl -> ntns:Vernacexpr.decl_notation list -> rec_declaration:Constr.rec_declaration -> possible_indexes:int list list option -> ?⁠restrict_ucontext:bool -> Recthm.t list -> Names.GlobRef.t list
val prepare_obligation : ?⁠opaque:bool -> ?⁠inline:bool -> name:Names.Id.t -> poly:bool -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
val prepare_parameter : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -> Evd.evar_map * Entries.parameter_entry
exception AlreadyDeclared of string option * Names.Id.t