Module `Declare.Proof`

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

val get_proof : t -> Proof.t: XXX: These are internal and will go away from publis API once lemmas is merged here

val get_proof_name : t -> Names.Id.t
val get_used_variables : t -> Names.Id.Set.t option: XXX: These 3 are only used in lemmas

val get_universe_decl : t -> UState.universe_decl
val get_initial_euctx : t -> UState.t
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 * t: Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it)

val compact : t -> t
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.