Module `Pfedit`

Global proof state. A quite redundant wrapper on Proof_global.

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_proof_context : Proof.t -> Evd.evar_map * Environ.env: get_proof_context () gets the goal context for the first subgoal of the proof

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 build_constant_by_tactic : name:Names.Id.t -> ?⁠opaque:Proof_global.opacity_flag -> UState.t -> Environ.named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic -> Evd.side_effects Declare.proof_entry * bool * UState.t
val build_by_tactic : ?⁠side_eff:bool -> Environ.env -> UState.t -> poly:bool -> 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.