Module Proof_global

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

type t
val get_proof : t -> Proof.t
val get_proof_name : t -> Names.Id.t
val get_used_variables : t -> Names.Id.Set.t option
val get_universe_decl : t -> UState.universe_decl

Get the universe declaration associated to the current proof.

val get_initial_euctx : t -> UState.t

Get initial universe state

val compact_the_proof : t -> t
type proof_object = {
name : Names.Id.t;

name of the proof

entries : Evd.side_effects Declare.proof_entry list;

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

poly : bool;

polymorphic status

universes : UState.t;

universe state

udecl : UState.universe_decl;

universe declaration

}

When a proof is closed, it is reified into a proof_object

type 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 -> 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 -> 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 -> proof_object
type closed_proof_output = (Constr.t * Evd.side_effects) 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 -> proof_object
val get_open_goals : t -> int
val map_proof : (Proof.t -> Proof.t) -> t -> t
val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
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