# Module `Declare.Proof`

`Declare.Proof.t`

Construction of constants using interactive proofs.

`val start : info:Info.t -> cinfo:EConstr.t CInfo.t -> Evd.evar_map -> t`

`start_proof ~info ~cinfo sigma`

starts a proof of`cinfo`

. The proof is started in the evar map`sigma`

(which can typically contain universe constraints)

`val start_derive : f:Names.Id.t -> name:Names.Id.t -> info:Info.t -> Proofview.telescope -> t`

`start_{derive,equations}`

are functions meant to handle interactive proofs with multiple goals, they should be considered experimental until we provide a more general API encompassing both of them. Please, get in touch with the developers if you would like to experiment with multi-goal dependent proofs so we can use your input on the design of the new API.

`val start_equations : name:Names.Id.t -> info:Info.t -> hook:(pm:OblState.t -> Names.Constant.t list -> Evd.evar_map -> OblState.t) -> types:(Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list -> Evd.evar_map -> Proofview.telescope -> t`

`val start_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t -> Evd.evar_map -> t`

Pretty much internal, used by the Lemma vernaculars

`type mutual_info`

`= bool * lemma_possible_guards * Constr.t option list option`

`val start_mutual_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t list -> mutual_info:mutual_info -> Evd.evar_map -> int list option -> t`

Pretty much internal, used by mutual Lemma / Fixpoint vernaculars

`val save : pm:OblState.t -> proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list`

Qed a proof

`val save_regular : proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> Names.GlobRef.t list`

For proofs known to have

`Regular`

ending, no need to touch program state.

`val save_admitted : pm:OblState.t -> proof:t -> OblState.t`

Admit a proof

`val by : unit Proofview.tactic -> t -> t * bool`

`by tac`

applies tactic`tac`

to the 1st subgoal of the current focused proof. Returns`false`

if an unsafe tactic has been used.

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

`val fold : f:(Proof.t -> 'a) -> t -> 'a`

`val map : f:(Proof.t -> Proof.t) -> t -> t`

`val map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a`

`val map_fold_endline : f:(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 -> using:Proof_using.t -> 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 get_used_variables : t -> Names.Id.Set.t option`

Gets the set of variables declared to be used by the proof. None means no "Proof using" or #

`using`

was given

`val update_sigma_univs : UGraph.t -> t -> t`

Update the proof's universe information typically after a side-effecting command (e.g. a sublemma definition) has been run inside it.

`val get_open_goals : t -> int`

`val get_goal_context : t -> int -> Evd.evar_map * Environ.env`

`val get_current_goal_context : t -> Evd.evar_map * Environ.env`

`get_current_goal_context ()`

works as`get_goal_context 1`

`val get_current_context : t -> Evd.evar_map * Environ.env`

`get_current_context ()`

returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map.

### Proof delay API, warning, internal, not stable

`val return_proof : t -> closed_proof_output`

Requires a complete proof.

`val return_partial_proof : t -> closed_proof_output`

An incomplete proof is allowed (no error), and a warn is given if the proof is complete.

`type proof_object`

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

`val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object`

`val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object`

`val save_lemma_admitted_delayed : pm:OblState.t -> proof:proof_object -> OblState.t`

Special cases for delayed proofs, in this case we must provide the proof information so the proof won't be forced.

`val save_lemma_proved_delayed : pm:OblState.t -> proof:proof_object -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list`

`val get_po_name : proof_object -> Names.Id.t`

Used by the STM only to store info, should go away