Module Vernacstate.Proof_global

val get : unit -> Proof_global.t option
val set : Proof_global.t option -> unit
val freeze : marshallable:bool -> Proof_global.t option
val unfreeze : Proof_global.t -> unit
exception NoCurrentProof
val there_are_pending_proofs : unit -> bool
val get_open_goals : unit -> int
val set_terminator : Proof_global.proof_terminator -> unit
val give_me_the_proof : unit -> Proof.t
val give_me_the_proof_opt : unit -> Proof.t option
val get_current_proof_name : unit -> Names.Id.t
val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
val install_state : Proof_global.t -> unit
val return_proof : ?⁠allow_partial:bool -> unit -> Proof_global.closed_proof_output
val close_future_proof : opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> Proof_global.closed_proof
val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> Proof_global.closed_proof
val discard_all : unit -> unit
val update_global_env : unit -> unit
val get_current_context : unit -> Evd.evar_map * Environ.env
val get_all_proof_names : unit -> Names.Id.t list
val copy_terminators : src:Proof_global.t option -> tgt:Proof_global.t option -> Proof_global.t option