Module Pfedit

Global proof state. A quite redundant wrapper on Proof_global.

...
exception NoSuchGoal
val get_goal_context : Proof_global.t -> int -> Evd.evar_map * Environ.env
val get_current_goal_context : Proof_global.t -> Evd.evar_map * Environ.env

get_current_goal_context () works as get_goal_context 1

val get_current_context : Proof_global.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.

...
val solve : ?⁠with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool
val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
val use_unification_heuristics : unit -> bool

Option telling if unification heuristics should be used.

val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> Proof_global.t -> Proof_global.t
val build_constant_by_tactic : Names.Id.t -> UState.t -> Environ.named_context_val -> ?⁠goal_kind:Decl_kinds.goal_kind -> EConstr.types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * UState.t
val build_by_tactic : ?⁠side_eff:bool -> Environ.env -> UState.t -> ?⁠poly:Decl_kinds.polymorphic -> EConstr.types -> unit Proofview.tactic -> Constr.constr * bool * UState.t
val refine_by_tactic : name:Names.Id.t -> poly:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> Constr.constr * Evd.evar_map

A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.