# Module `Proof_global`

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

`val get_current_proof_name : t -> Names.Id.t`

`val get_current_persistence : t -> Decl_kinds.goal_kind`

`val get_all_proof_names : t -> Names.Id.t list`

`val discard : Names.lident -> t -> t option`

`val discard_current : t -> t option`

`val give_me_the_proof : t -> Proof.t`

`val compact_the_proof : t -> t`

`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.