Module `Proof_global`

This module defines proof facilities relevant to the toplevel. In particular it defines the global proof environment.

type lemma_possible_guards = int list list: When a proof is closed, it is reified into a proof_object, where id is the name of the proof, entries the list of the proof terms (in a form suitable for definitions). Together with the terminator function which takes a proof_object together with a proof_end (i.e. an proof ending command) and registers the appropriate values.

type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes : UState.t; }
type opacity_flag = | Opaque | Transparent
type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of opacity_flag * Names.lident option * proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator

val make_terminator : (proof_ending -> unit) -> proof_terminator
val apply_terminator : proof_terminator -> proof_ending -> unit
val start_proof : ontop:t option -> Evd.evar_map -> Names.Id.t -> ?⁠pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> t: start_proof ~ontop id str pl goals terminator starts a proof of name id with goals goals (a list of pairs of environment and conclusion); str describes what kind of theorem/definition this is; terminator is used at the end of the proof to close the proof (e.g. to declare the built constructions as a coercion or a setoid morphism). The proof is started in the evar map sigma (which can typically contain universe constraints), and with universe bindings pl.

val start_dependent_proof : ontop:t option -> Names.Id.t -> ?⁠pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> t: Like start_proof except that there may be dependencies between initial goals.

val update_global_env : t -> t: Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes there_are_pending_proofs.

val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof

type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t

val return_proof : ?⁠allow_partial:bool -> t -> closed_proof_output
val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> closed_proof
val get_terminator : t -> proof_terminator: Gets the current terminator without checking that the proof has been completed. Useful for the likes of Admitted.

val set_terminator : proof_terminator -> t -> t
val get_open_goals : t -> int
val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a: Runs a tactic on the current proof. Raises NoCurrentProof is there is no current proof. The return boolean is set to false if an unsafe tactic has been used.

val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t: Sets the tactic to be used when a tactic line is closed with ...

val set_used_variables : t -> Names.Id.t list -> (Constr.named_context * Names.lident list) * t: Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared

val get_used_variables : t -> Constr.named_context option
val get_universe_decl : t -> UState.universe_decl: Get the universe declaration associated to the current proof.